Mathlib.Data.Finsupp.Order._auxLemma.14
theorem Mathlib.Data.Finsupp.Order._auxLemma.14 :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {a : α}, (a ∈ f.support) = (f a ≠ 0)
This theorem, `Mathlib.Data.Finsupp.Order._auxLemma.14`, states that for any type `α`, any type `M` that has a zero element (`inst : Zero M`), a function `f` from `α` to `M` and an element `a` of type `α`, `a` is in the support of `f` if and only if the function `f` applied to `a` is not equal to zero. In other words, the support of a function `f` in this context is the set of elements `a` such that `f(a)` is not zero.
More concisely: The theorem `Mathlib.Data.Finsupp.Order._auxLemma.14` in Lean 4 states that for any function `f` from type `α` to a type `M` with a zero element, the element `a` is in the support of `f` if and only if `f(a)` is non-zero.
|
Finsupp.single_le_iff
theorem Finsupp.single_le_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddCommMonoid α] {i : ι} {x : α} {f : ι →₀ α},
(fun₀ | i => x) ≤ f ↔ x ≤ f i
This theorem, `Finsupp.single_le_iff`, states that for any types `ι` and `α`, given the instance of `α` as a canonically ordered additive commutative monoid, and any element `i` of `ι`, `x` of `α`, and function `f` from `ι` to `α`, the function that maps `i` to `x` is less than or equal to `f` if and only if `x` is less than or equal to the value of `f` at `i`. In other words, a single element `x` is less than or equal to a function `f` if and only if `x` is less than or equal to the value of `f` at a specific point `i`.
More concisely: For any type `ι`, `α` with `α` an ordered additive commutative monoid, and `i ∈ ι`, `x ∈ α`, and `f : ι → α`, `x ≤ f i` if and only if `f i ≤ x`.
|
Finsupp.coe_le_coe
theorem Finsupp.coe_le_coe :
∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : LE α] {f g : ι →₀ α}, ⇑f ≤ ⇑g ↔ f ≤ g
This theorem states that for any types `ι` and `α`, where `α` has a zero and a less-than-or-equal-to (`≤`) operation, and for any two functions `f` and `g` from `ι` to `α` that have finite support (`ι →₀ α`), the pointwise application of `f` is less than or equal to the pointwise application of `g` if and only if `f` is less than or equal to `g`. In other words, the ordering of the functions `f` and `g` is the same as the ordering of their pointwise applications.
More concisely: For functions `f` and `g` from type `ι` to type `α` with finite support, where `α` is equipped with a zero `0` and a `≤` relation, the pointwise application `∀ i, f i ≤ g i` if and only if `f ≤ g`.
|