DFinsupp.card_Icc
theorem DFinsupp.card_Icc :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
[inst_2 : (i : ι) → PartialOrder (α i)] [inst_3 : (i : ι) → Zero (α i)]
[inst_4 : (i : ι) → LocallyFiniteOrder (α i)] (f g : Π₀ (i : ι), α i),
(Finset.Icc f g).card = (f.support ∪ g.support).prod fun i => (Finset.Icc (f i) (g i)).card
The theorem `DFinsupp.card_Icc` states that for any types `ι` and `α` (where `α` is indexed by `ι`), given decidable equality on `ι` and each `α i`, a partial order on each `α i`, a zero for each `α i`, and a locally finite order on each `α i`, for any two functions `f` and `g` that map from `ι` to `α i`, the cardinality of the finset of elements between `f` and `g` (inclusive) equals the product, as `i` ranges over the union of the support of `f` and the support of `g`, of the cardinality of the finset of elements between `f i` and `g i` (inclusive).
In other words, the size of the set of elements between two functions `f` and `g` can be computed as a product of sizes of sets between their corresponding elements.
More concisely: For functions between indexed types with decidable equality, partial order, zero, and locally finite order structures, the cardinality of their elements between the functions is equal to the product of cardinalities of elements between corresponding functions.
|
Finset.mem_dfinsupp_iff_of_support_subset
theorem Finset.mem_dfinsupp_iff_of_support_subset :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (α i)] {s : Finset ι}
{f : Π₀ (i : ι), α i} [inst_2 : (i : ι) → DecidableEq (α i)] {t : Π₀ (i : ι), Finset (α i)},
t.support ⊆ s → (f ∈ s.dfinsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i)
The theorem `Finset.mem_dfinsupp_iff_of_support_subset` states that for any type `ι` and a suite of types `α` indexed by `ι`, given a decidable equality on `ι` and each `α i` having a zero element, for any finite set `s` of `ι`, a function `f` from `ι` to `α i`, and a function `t` from `ι` to a finite set of `α i` such that the support of `t` is a subset of `s`, `f` belongs to the `dfinsupp` (directed family of finite supports) of `s` by `t` if and only if for every `i` in `ι`, the value of `f` at `i` belongs to `t i`.
In simpler terms, it indicates that when the function `t` is supported on `s`, a function `f` is in the directed family of finite supports of `s` by `t` exactly when `f` is pointwise in `t`, i.e., every value of `f` is in the corresponding set given by `t`.
More concisely: For any type `ι` and a suite of types `α` indexed by `ι`, given a decidable equality on `ι` and each `α i` having a zero element, a function `f` from `ι` to `α i` belongs to the `dfinsupp` of `s` by `t`, where `s` is a finite set of `ι` and `t` is a function from `ι` to finite sets of `α i` with support in `s`, if and only if for all `i` in `ι`, `f i` is in `t i`.
|