Finsupp.card_Icc

theorem Finsupp.card_Icc : ∀ {ι : Type u_1} {α : Type u_2} [inst : PartialOrder α] [inst_1 : Zero α] [inst_2 : LocallyFiniteOrder α] (f g : ι →₀ α), (Finset.Icc f g).card = (f.support ∪ g.support).prod fun i => (Finset.Icc (f i) (g i)).card

This theorem states that for any two functions `f` and `g` from a type `ι` to a type `α` which have a partial order, a zero, and a locally finite order, the size (or cardinality) of the finite set formed by including all elements `x` such that `f(x) ≤ x ≤ g(x)` is equal to the product of the sizes of the finite sets formed by including all elements `x` such that `f(i) ≤ x ≤ g(i)`, where `i` ranges over the elements in the union of the supports of `f` and `g`. The support of a function is the set of points where the function is non-zero. In mathematical terms, if $\text{Icc}$ is the interval $[f(x), g(x)]$ and $\text{card}$ denotes the cardinality of a set, the theorem is stated as: $$\text{card}(\text{Icc}(f,g)) = \prod_{i \in \text{support}(f) \cup \text{support}(g)} \text{card}(\text{Icc}(f(i),g(i)))$$

More concisely: The cardinality of the set of elements between the images of two functions with a partial order, zero, and locally finite order is equal to the product of the cardinalities of the sets between their images at each support element.