Mathlib.Data.DFinsupp.Order._auxLemma.16
theorem Mathlib.Data.DFinsupp.Order._auxLemma.16 :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
[inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} {i : ι}, (i ∈ f.support) = (f i ≠ 0)
This theorem, named `Mathlib.Data.DFinsupp.Order._auxLemma.16`, states that for any type `ι`, for any function `β` mapping `ι` to another type, given that equality on `ι` is decidable, that for any `i` of type `ι` there exists a zero element in `β i`, and that for any `i` in `ι` and any `x` in `β i` it is decidable whether `x` is not equal to zero, then for any function `f` of type `Π₀ (i : ι), β i` (a function that takes in `i` from `ι` and outputs an element from `β i`), and any `i` of type `ι`, `i` is in the support set of `f` if and only if the function `f` evaluated at `i` is not equal to zero.
In simpler words, this theorem says that an element `i` is in the support set of a function `f` (i.e., it is a point where `f` is non-zero) if and only if `f(i)` is not zero. The support set is defined for functions that map from a type `ι` to another type through a function `β`, where it is decidable whether elements are equal in `ι` and whether elements are zero in `β i`.
More concisely: For any function `f` mapping a decidably-equaled type `ι` to another type `β` with decidable zero tests, the support set of `f` equals {`i` in `ι` | `f i` ≠ 0}.
|
DFinsupp.coe_le_coe
theorem DFinsupp.coe_le_coe :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → LE (α i)]
{f g : Π₀ (i : ι), α i}, ⇑f ≤ ⇑g ↔ f ≤ g
This theorem states that for any types `ι` and `α` (where `α` is a function of `ι`), given a zero instance for `α i` and a less-than-or-equal-to (≤) instance for `α i` for each `i` in `ι`, the function application of a direct sum function `f` is less than or equal to the function application of another direct sum function `g` if and only if `f` is less than or equal to `g`.
Here, `f` and `g` are represented as `Π₀ (i : ι), α i`, which means they are direct sum functions over the index set `ι` with values in the type `α i`. The direct sum is a generalization of the sum concept, where the sum of a family of elements is only dependent on a finite number of them.
More concisely: For any types `ι` and `α`, given zero and ≤ instances for `α i` (for all `i` in `ι`), the direct sum functions `Π₀ (i : ι), α i` `f` and `g` satisfy `f ≤ g` if and only if `∀i, f i ≤ g i`.
|