Finsupp.mapRange_single
theorem Finsupp.mapRange_single :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} [inst : Zero M] [inst_1 : Zero N] {f : M → N} {hf : f 0 = 0} {a : α}
{b : M}, (Finsupp.mapRange f hf fun₀ | a => b) = fun₀ | a => f b
This theorem states that for any types `α`, `M` and `N`, given a function `f` mapping from `M` to `N` that preserves zero (meaning `f` of zero equals zero), and any elements `a` of type `α` and `b` of type `M`, the `mapRange` function applied to a singleton function (a function that maps `a` to `b` and everything else to zero) equals a singleton function that maps `a` to `f(b)`. The `mapRange` function is essentially mapping `f` across all values in the range of the singleton function, but since the only non-zero value in the range is `b`, it only affects the mapping of `a`.
More concisely: For any types `α`, `M`, `N`, and functions `f : M -> N` preserving zero, `mapRange (λ x => if h : x = a then b else 0) (singleton a) = singleton (f b) : α -> N`, where `a : α` and `b : M`.
|
Finsupp.support_single_subset
theorem Finsupp.support_single_subset :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M}, (fun₀ | a => b).support ⊆ {a}
This theorem states that for any types `α` and `M` where `M` is a zero type, and for any elements `a` of type `α` and `b` of type `M`, the support of the function `fun₀` that maps `a` to `b` is a subset of the set containing `a`. In other words, the only element that possibly has a non-zero image under `fun₀` is `a`.
More concisely: For any type `M` that is a zero type and any function `f : α → M` with `α` being an arbitrary type and `f a` being the only non-zero element for some `a` in `α`, the support of `f` is equal to `{a}`.
|
Finsupp.single_add
theorem Finsupp.single_add :
∀ {α : Type u_1} {M : Type u_5} [inst : AddZeroClass M] (a : α) (b₁ b₂ : M),
(fun₀ | a => b₁ + b₂) = (fun₀ | a => b₁) + fun₀ | a => b₂
This theorem states that for any type `α`, a second type `M` that forms an additive monoid, and any elements `a` from `α`, `b₁` and `b₂` from `M`, the finitely supported function `fun₀` that maps `a` to the sum of `b₁` and `b₂` is equal to the sum of the finitely supported function `fun₀` that maps `a` to `b₁` and the finitely supported function `fun₀` that maps `a` to `b₂`. That is, the function behaves linearly with respect to addition in `M`. The `Finsupp.single_add` theorem essentially captures the distributive law for functions.
More concisely: For any type `α`, any additive monoid `M`, and any `a` in `α` and `b₁, b₂` in `M`, the finitely supported function mapping `a` to `b₁ + b₂` is equal to the sum of the functions mapping `a` to `b₁` and `a` to `b₂`.
|
Finsupp.add_apply
theorem Finsupp.add_apply :
∀ {α : Type u_1} {M : Type u_5} [inst : AddZeroClass M] (g₁ g₂ : α →₀ M) (a : α), (g₁ + g₂) a = g₁ a + g₂ a := by
sorry
This theorem, `Finsupp.add_apply`, states that for any two functions `g₁` and `g₂` which map elements from a certain type `α` to a type `M` (which has an addition operation and a zero element), and for any element `a` of type `α`, the sum of `g₁` and `g₂` at `a` is equal to the sum of the values of `g₁` at `a` and `g₂` at `a`. This is essentially asserting that addition of functions obeys the same properties as addition of their values.
More concisely: For functions `g₁` and `g₂` from type `α` to additive type `M`, and for all `a` in `α`, `(g₁ + g₂) a = g₁ a + g₂ a`.
|
Finsupp.support_add
theorem Finsupp.support_add :
∀ {α : Type u_1} {M : Type u_5} [inst : AddZeroClass M] [inst_1 : DecidableEq α] {g₁ g₂ : α →₀ M},
(g₁ + g₂).support ⊆ g₁.support ∪ g₂.support
The theorem `Finsupp.support_add` asserts that for any types `α` and `M`, where `M` forms an `AddZeroClass` (i.e., it has both an additive identity and an addition operation) and `α` has decidable equality, given two functions `g₁` and `g₂` from `α` to `M`, the support of the sum of `g₁` and `g₂` (denoted as `g₁ + g₂`) is a subset of the union of the support of `g₁` and the support of `g₂`. Here, the term "support" refers to the set of points where the function is non-zero.
More concisely: For functions `g₁` and `g₂` from a decidably equal type `α` to an additive semigroup `M`, the support of `g₁ + g₂` is contained in the union of the supports of `g₁` and `g₂`.
|
Finsupp.embDomain_apply
theorem Finsupp.embDomain_apply :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ↪ β) (v : α →₀ M) (a : α),
(Finsupp.embDomain f v) (f a) = v a
The theorem `Finsupp.embDomain_apply` states that for any types `α`, `β`, and `M` where `M` has a zero, and for any function `f` that embeds `α` into `β` and for any finitely supported function `v` from `α` to `M`, the value of the function `Finsupp.embDomain f v` at `f a` is equal to `v a` for any `a` in `α`. In other words, the value of `v a` is transported to `f a` in the finitely supported function created by `Finsupp.embDomain`.
More concisely: For any function `f: α -> β` embedding `α` into a type `β` with a zero, and any finitely supported function `v: α -> M` from a type `α` to a type `M` with a zero, `Finsupp.embDomain f v a = v a` for all `a` in `α`.
|
Finsupp.induction_linear
theorem Finsupp.induction_linear :
∀ {α : Type u_1} {M : Type u_5} [inst : AddZeroClass M] {p : (α →₀ M) → Prop} (f : α →₀ M),
p 0 → (∀ (f g : α →₀ M), p f → p g → p (f + g)) → (∀ (a : α) (b : M), p fun₀ | a => b) → p f
This theorem is a principle of mathematical induction for finite function support (`Finsupp`) in a linear setting. Given any type `α`, another type `M` that has an additive zero class structure (meaning it has operations of addition and zero), and a property `p` that applies to functions from `α` into `M` with finite support, the theorem states that if the property holds for the zero function, and if the property is preserved under addition of such functions, and if the property holds for all 'singleton' functions that take a specific value from `α` to a specific value from `M`, then the property holds for all such functions with finite support.
More concisely: Given a type `α`, a type `M` with additive zero class structure, and a property `p` on functions from `α` to `M` with finite support, if `p` holds for the zero function, is closed under addition, and holds for all singleton functions, then `p` holds for all functions with finite support.
|
Finsupp.ext
theorem Finsupp.ext : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f g : α →₀ M}, (∀ (a : α), f a = g a) → f = g
This theorem, `Finsupp.ext`, establishes that for any types `α` and `M`, given `M` has zero element, if we have two functions `f` and `g` from `α` to `M` with support (considered as finitely supported functions), and for every `a` in `α`, `f` of `a` equals `g` of `a`, then it implies that function `f` is equal to function `g`. In other words, two finitely supported functions are considered equal if they return the same result for every element in the domain.
More concisely: If two finitely supported functions from a type to a type with zero element have equal values at every domain element, then they are equal.
|
Finsupp.single_apply
theorem Finsupp.single_apply :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {b : M} [inst_1 : Decidable (a = a')],
(fun₀ | a => b) a' = if a = a' then b else 0
The theorem `Finsupp.single_apply` states that for any types `α` and `M` with `M` being a type having a zero element, and for any values `a`, `a'` of type `α` and `b` of type `M`, where whether `a` equals `a'` is decidable, the function `fun₀` that maps `a` to `b` and everything else to zero, when applied to `a'`, gives `b` if `a` equals `a'` and gives zero otherwise.
More concisely: For types `α` and `M` with `M` having a zero element, and decidably equal `α` values `a` and `a'`, the function mapping `a` to `b` in `M` and everything else to zero yields `b` if `a = a'` and zero otherwise.
|
Finsupp.update_idem
theorem Finsupp.update_idem :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α) (b c : M),
(f.update a b).update a c = f.update a c
The theorem `Finsupp.update_idem` states that for any elements `a` of type `α` and `b`, `c` of type `M` (where `M` has a zero element), and any function `f` mapping elements of type `α` to elements of `M` (with finite support), updating the value of `f` at `a` to `b` and then updating it again at `a` to `c` is the same as just updating the value of `f` at `a` to `c` in the first place. In other words, consecutive updates at the same location in a finitely-supported function are idempotent; the second update erases the effect of the first.
More concisely: For any function `f` with finite support from type `α` to type `M` with zero element, the updates `f := (f.map (λ x => if x = a then b else f x))` and `f := (f.map (λ x => if x = a then c else f x))` are equal, where `a` is an element of type `α` and `b` and `c` are elements of type `M`.
|
Finsupp.erase_eq_update_zero
theorem Finsupp.erase_eq_update_zero :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α), Finsupp.erase a f = f.update a 0
This theorem states that for any types `α` and `M` where `M` has an instance of `Zero`, and for any finitely supported function `f` from `α` to `M`, and any value `a` from `α`, the operation of erasing `a` from `f` is identical to the operation of updating `f` at `a` with the value `0`. In other words, erasing `a` from the function `f` (making `f(a)` equal to `0`) is the same as explicitly updating `f(a)` to `0`.
More concisely: For any type `α`, type `M` with `Zero` instance, finitely supported function `f:` `α` `->` `M`, and `a` `∈` `α`, erasing `a` from `f` (setting `f a` to `0`) is equivalent to updating `f` at `a` with `0` (`f.update a 0`).
|
Finsupp.single_eq_update
theorem Finsupp.single_eq_update :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : DecidableEq α] (a : α) (b : M),
(⇑fun₀ | a => b) = Function.update 0 a b
The theorem `Finsupp.single_eq_update` states that for any types `α` and `M`, where `M` is a type with a defined zero element and `α` has decidable equality, for any elements `a` of type `α` and `b` of type `M`, the function that maps `a` to `b` and everything else to zero is the same as the function obtained by updating the zero function at `a` with the value `b`. In other words, creating a function that is zero everywhere except at `a` where it is `b` can be achieved in two ways: either directly defining it as such, or by taking the zero function and updating its value at `a` to `b`, and these two methods yield the same result. This theorem can be useful in functional programming and mathematical contexts where sparse representations are used (like in the case of the `Finsupp` or "finite support" structure in Lean).
More concisely: For any type `α` with decidable equality and type `M` with a zero element, the function mapping `a` to `b` and zero to all other elements of `α × M` equals the function obtained by updating the zero function at `a` with `b`.
|
Finsupp.support_erase
theorem Finsupp.support_erase :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : DecidableEq α] {a : α} {f : α →₀ M},
(Finsupp.erase a f).support = f.support.erase a
The theorem `Finsupp.support_erase` states that for any type `α` and `M` where `M` is a zero type and `α` has decidable equality, given any element `a` of type `α` and a function `f` from `α` to `M` with finite support, the support of the function obtained by erasing `a` from `f` is the same as the set obtained by erasing `a` from the support of `f`. In simpler terms, it asserts that erasing an element from a function with finite support only affects the values at that specific element, but the rest of the support remains the same.
More concisely: For any type `α` with decidable equality and any function `f` from `α` to a zero type with finite support, the support of `f` with an element `a` erased is equal to the support of `f` without `a` erased.
|
Finsupp.single_zero
theorem Finsupp.single_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α), (fun₀ | a => 0) = 0
This theorem states that for any type `α` and another type `M` equipped with a zero, if we construct a finitely supported function (also known as a `Finsupp`) that gives each element of type `α` the value zero, the result is equivalent to the zero finitely supported function. In other words, every singleton `Finsupp` that maps an element to zero is the zero `Finsupp`.
More concisely: For any type `α` and any finitely supported function `f : α →₀ ℤ`, the singleton function mapping an element `x : α` to zero `0 : ℤ` is equal to the zero finitely supported function `0 : α →₀ ℤ`.
|
Finsupp.single_eq_zero
theorem Finsupp.single_eq_zero :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M}, (fun₀ | a => b) = 0 ↔ b = 0
The theorem `Finsupp.single_eq_zero` states that for any types `α` and `M` with `M` being a type with a zero, and for any elements `a` of type `α` and `b` of type `M`, the function `fun₀` that maps `a` to `b` is equal to zero if and only if `b` is equal to zero. In other words, the function is null only when it maps `a` to the zero element of `M`.
More concisely: For any types `α` and `M` with `M` having a zero element, and for all `a : α` and `b : M`, the function mapping `a` to `b` is equal to the zero element of `M` if and only if `b` is equal to the zero element of `M`.
|
Finsupp.support_neg
theorem Finsupp.support_neg :
∀ {α : Type u_1} {G : Type u_9} [inst : AddGroup G] (f : α →₀ G), (-f).support = f.support
This theorem, `Finsupp.support_neg`, states that for any type `α` and an additive group `G`, the support of the negation of a function `f` from `α` to `G` is equal to the support of `f` itself. Here, "support" refers to the set of elements from `α` that the function `f` maps to non-zero elements in `G`. The negation of the function `f` is simply the function that maps each element to the additive inverse of its image under `f`.
More concisely: For any function `f` from type `α` to an additive group `G`, the support of `f` and the support of the negation of `f` are equal.
|
Finsupp.not_mem_support_iff
theorem Finsupp.not_mem_support_iff :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {a : α}, a ∉ f.support ↔ f a = 0
This theorem states that for any given types `α` and `M`, where `M` has an instance of `Zero`, and for any function `f` from `α` to `M` and any element `a` of `α`, `a` is not in the support of `f` if and only if the value of function `f` at `a` is zero. In other words, an element `a` does not belong to the support of a function `f` if applying `f` to `a` yields zero.
More concisely: For any function `f` from type `α` to a type `M` with instance of `Zero`, an element `a` in `α` is not in the support of `f` if and only if `f a` equals `0`.
|
Mathlib.Data.Finsupp.Defs._auxLemma.8
theorem Mathlib.Data.Finsupp.Defs._auxLemma.8 : (¬False) = True
This theorem, `Mathlib.Data.Finsupp.Defs._auxLemma.8`, asserts that the negation of `False` equals `True`. In mathematical logic, this is a basic truth, stating that if something is not false, then it must be true.
More concisely: The negation of False is equal to True. (In mathematical logic, ⊢ ⊥ → ⊥' where ⊥ is the proposition of False and ⊥' is the proposition of True.)
|
Finsupp.mapRange_id
theorem Finsupp.mapRange_id :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (g : α →₀ M), Finsupp.mapRange id ⋯ g = g
This theorem, `Finsupp.mapRange_id`, states that for any type `α` and any type `M` that has an instance of `Zero`, the function `Finsupp.mapRange id` applied to any function `g` (from `α` to `M`) is equal to `g` itself. In other words, mapping the identity function over the range of a function doesn't change the function.
More concisely: For any type `α` and any function `g : α → M` where `M` has an instance of `Zero`, `Finsupp.mapRange id g` equals `g`.
|
Finsupp.coe_zero
theorem Finsupp.coe_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M], ⇑0 = 0
This theorem, `Finsupp.coe_zero`, states that for any types `α` and `M` where `M` is equipped with a zero element, the function obtained by applying the coercion function `⇑` to the zero element of the type of finitely supported functions from `α` to `M` is equivalent to the zero function. In other words, the zero finitely supported function maps every element to zero.
More concisely: The coercion of the zero element in a type equipped with a zero element to the type of finitely supported functions maps every element to the zero value in the codomain.
|
Finsupp.single_left_injective
theorem Finsupp.single_left_injective :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {b : M}, b ≠ 0 → Function.Injective fun a => fun₀ | a => b := by
sorry
The theorem `Finsupp.single_left_injective` states that for any types `α` and `M`, with `M` being a type with a zero element, and any element `b` of `M` that is not equal to zero, the function `Finsupp.single` that takes an element `a` of type `α` and maps it to a function that returns `b` for all inputs equal to `a` and zero otherwise, is injective in `a`. In other words, if two different elements `a1` and `a2` of type `α` are mapped to the same function by `Finsupp.single a b`, then `a1` must be equal to `a2`. The injectiveness in `b` is addressed in another theorem, namely `Finsupp.single_injective`.
More concisely: If `α` is a type and `M` is a type with a zero element `b ≠ 0`, then the function `Finsupp.single a b` mapping `α` to the constant function with value `b` at `a` and zero elsewhere is injective on `α`.
|
Finsupp.addHom_ext'
theorem Finsupp.addHom_ext' :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
⦃f g : (α →₀ M) →+ N⦄, (∀ (x : α), f.comp (Finsupp.singleAddHom x) = g.comp (Finsupp.singleAddHom x)) → f = g
This theorem states that if there are two additive homomorphisms from `α →₀ M` to `N`, denoted as `f` and `g`, and for every `x` in `α`, the composition of `f` with `Finsupp.singleAddHom x` is equal to the composition of `g` with `Finsupp.singleAddHom x`, then `f` and `g` must be equal.
The theorem is formulated using equality of `AddMonoidHom`s, which means it is particularly amenable to the `ext` tactic. This tactic can apply a type-specific extensionality lemma after applying this theorem. For example, if the fiber `M` is `ℕ` or `ℤ`, it is enough to verify that `f` and `g` are equal on elements of the form `single a 1`.
More concisely: If two additive homomorphisms from one additive monoid to another satisfy the condition that the composition of each homomorphism with the additive homomorphism defined by a single element is equal, then the two homomorphisms are equal.
|
Mathlib.Data.Finsupp.Defs._auxLemma.1
theorem Mathlib.Data.Finsupp.Defs._auxLemma.1 :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {a : α}, (a ∈ f.support) = (f a ≠ 0)
This theorem states that for any type `α` and any type `M` that has a zero element, given a function `f` from `α` to `M` and an element `a` of `α`, the element `a` is in the support of `f` if and only if the value of `f` at `a` is not zero. Here, the support of `f` is the set of elements of `α` for which `f` does not return zero.
More concisely: For any function `f` from type `α` to a type `M` with zero element, the element `a` in `α` is in the support of `f` if and only if `f a ≠ 0`.
|
Finsupp.single_eq_single_iff
theorem Finsupp.single_eq_single_iff :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a₁ a₂ : α) (b₁ b₂ : M),
((fun₀ | a₁ => b₁) = fun₀ | a₂ => b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
The theorem `Finsupp.single_eq_single_iff` states that for any types `α` and `M` with `M` being a type with zero, given any four elements `a₁`, `a₂` of type `α` and `b₁`, `b₂` of type `M`, the function `fun₀ | a₁ => b₁` is equal to the function `fun₀ | a₂ => b₂` if and only if either `a₁` equals `a₂` and `b₁` equals `b₂`, or `b₁` equals zero and `b₂` equals zero. This theorem essentially describes the conditions for equality between two functions constructed using the `Finsupp.single` function, which constructs a function that maps a single element to a nonzero value and all other elements to zero.
More concisely: For functions `f` and `g` constructed as `Finsupp.single a b` with `a` from type `α` and `b` from type `M` with zero, `f = g` if and only if `a = a'` and `b = b'` or `b = 0` and `b' = 0`.
|
Finsupp.coe_add
theorem Finsupp.coe_add : ∀ {α : Type u_1} {M : Type u_5} [inst : AddZeroClass M] (f g : α →₀ M), ⇑(f + g) = ⇑f + ⇑g
This theorem states that for any two functions `f` and `g` of type `α →₀ M`, where `M` is a type with an addition and zero operation (`AddZeroClass`), the operation of applying the function `(f + g)` is equivalent to separately applying and then adding the results of functions `f` and `g`. In mathematical terms, for all `α` in `Type u_1` and `M` in `Type u_5` with `AddZeroClass` structure, the function application of the sum of `f` and `g` is equal to the sum of the function applications of `f` and `g`.
More concisely: For any functions `f` and `g` of type `α →₀ M` with `M` being an `AddMonoid`, the function `(f + g)` equals the application of `f` followed by `g` and the addition of their results.
|
Finsupp.erase_ne
theorem Finsupp.erase_ne :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {f : α →₀ M}, a' ≠ a → (Finsupp.erase a f) a' = f a'
The theorem `Finsupp.erase_ne` states that for any types `α` and `M` (where `M` has an instance of zero), given any `a` and `a'` of type `α` and a finitely supported function `f` from `α` to `M`, if `a'` is not equal to `a`, then the value of the function `Finsupp.erase a f` at `a'` is equal to the value of the function `f` at `a'`. In other words, erasing `a` from the function `f` does not change the value of `f` at any other points.
More concisely: For any type `α` and `M` with a zero instance, and any finitely supported function `f` from `α` to `M`, `Finsupp.erase a f a' = f a'` for all `a ≠ a'` in `α`.
|
Finsupp.coe_neg
theorem Finsupp.coe_neg : ∀ {α : Type u_1} {G : Type u_9} [inst : NegZeroClass G] (g : α →₀ G), ⇑(-g) = -⇑g
This theorem states that for any type `α` and any type `G` that has a `NegZeroClass` instance (i.e., `G` has operations for negation and zero), and for any function `g` from `α` to `G`, negating the function `g` (denoted as `-g`) and then applying it (denoted as `⇑(-g)`) is the same as first applying `g` and then negating the result (denoted as `-⇑g`). Essentially, it asserts that the order of negation and function application does not matter.
More concisely: For any function `g` from type `α` to a type `G` with `NegZeroClass`, the functions `neg ∘ g` and `g ∘ neg` are equal, where `neg` denotes negation in `G`.
|
Finsupp.single_eq_set_indicator
theorem Finsupp.single_eq_set_indicator :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M}, (⇑fun₀ | a => b) = {a}.indicator fun x => b := by
sorry
The theorem `Finsupp.single_eq_set_indicator` states that for any types `α` and `M` with `M` having a zero element, and for any elements `a` of type `α` and `b` of type `M`, the function provided by the single-element finite support function at `a` with value `b` is equivalent to the set indicator function applied on a set containing only `a` and mapping each element `x` to `b`. In other words, the function that maps `a` to `b` and everything else to `0` is the same whether it's implemented with a finite support function or a set indicator function.
More concisely: For any types `α` and `M` with `M` having a zero element, and for any `a : α` and `b : M`, the single-element finite support function at `a` with value `b` equals the set indicator function of the singleton set `{a}`, both mapping everything outside `a` to `0`.
|
Finsupp.update_self
theorem Finsupp.update_self :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α), f.update a (f a) = f
The theorem `Finsupp.update_self` states that for any type `α`, any type `M` with a zero element, any finitely supported function `f` from `α` to `M`, and any element `a` of type `α`, updating `f` at `a` with the value `f(a)` leaves `f` unchanged. In simpler terms, if we update the function at a specific point with the function's value at that point, then the function does not change.
More concisely: For any type `α`, any type `M` with a zero element, and any finitely supported function `f:` `α` `→` `M`, `f` is equal to the function obtained by updating `f` at `a` with the value `f(a)` for all `a` in `α`.
|
Finsupp.single_injective
theorem Finsupp.single_injective :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α), Function.Injective (Finsupp.single a)
The theorem `Finsupp.single_injective` states that for any type `α` and any type `M` with an instance of the `Zero` typeclass, the function `Finsupp.single a`, where `a` is an element of `α`, is injective. In other words, if `Finsupp.single a b1` is equal to `Finsupp.single a b2`, then `b1` must be equal to `b2`. This theorem is only about injectivity in the second argument of `Finsupp.single`. For the statement of injectivity in the first argument, refer to the theorem `Finsupp.single_left_injective`.
More concisely: For any type `α` and `M` with an instance of `Zero`, the function `Finsupp.single a` from `α` to `M Key α → M` is injective in its second argument `b`.
|
Finsupp.erase_of_not_mem_support
theorem Finsupp.erase_of_not_mem_support :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {a : α}, a ∉ f.support → Finsupp.erase a f = f := by
sorry
The theorem `Finsupp.erase_of_not_mem_support` states that for any type `α` and any type `M` with a zero element (indicated by `Zero M`), if you have a finitely supported function `f : α →₀ M` and an element `a : α` that is not in the support of `f` (i.e., `f(a) = 0`), then erasing `a` from `f` using the `Finsupp.erase` function does not change `f`. In other words, if `a` does not contribute to the finitely supported function `f`, then removing `a` leaves `f` unchanged.
More concisely: For any type `α` and type `M` with a zero element, if `f : α →₀ M` is a finitely supported function and `a : α` is not in the support of `f`, then `Finsupp.erase a f = f`.
|
Finsupp.embDomain_notin_range
theorem Finsupp.embDomain_notin_range :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ↪ β) (v : α →₀ M),
∀ a ∉ Set.range ⇑f, (Finsupp.embDomain f v) a = 0
The theorem `Finsupp.embDomain_notin_range` states that for any types `α`, `β`, and `M` with `M` having a zero element, given an injective function `f : α ↪ β` and a finitely supported function `v : α →₀ M`, if an element `a` of type `β` is not in the range of the function `f`, then applying the function `Finsupp.embDomain f v` to `a` yields the zero element of type `M`. In other words, the function `Finsupp.embDomain f v` maps elements of `β` not reachable by `f` to zero.
More concisely: For any injective function `f : α ↪ β`, finitely supported function `v : α →₀ M`, and `a ∈ β` not in the image of `f`, `Finsupp.embDomain f v a = 0`.
|
Finsupp.support_zero
theorem Finsupp.support_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M], Finsupp.support 0 = ∅
This theorem states that for any type `α` and `M`, where `M` has a zero element, the support of the zero function (represented as 0) is an empty set. In other words, there are no elements `α` for which the zero function gives a non-zero value in `M`.
More concisely: For any type `α` and additive monoid `M` with zero element, the zero function maps all elements of `α` to the zero element in `M`, implying its support is the empty set.
|
Finsupp.coe_update
theorem Finsupp.coe_update :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α) (b : M) [inst_1 : DecidableEq α],
⇑(f.update a b) = Function.update (⇑f) a b
This theorem states that for any types `α` and `M` with `M` having an instance of the zero element, a given function `f` from `α` to `M` with finite support, a point `a` of type `α`, a value `b` of type `M`, and `α` having a decidable equality, applying `Finsupp.update` on `f` at point `a` with value `b` and then getting the result function is equivalent to first getting the function of `f` and then applying `Function.update` at point `a` with value `b`. In other words, updating a finitely supported function and then extracting the function is the same as first extracting the function and then updating it.
More concisely: For functions `f : α → M` with finite support from a decidably equal type `α` to a type `M` with a zero element, updating `f` at point `a` with value `b` using `Finsupp.update` is equivalent to first extracting the function `g = f.get` and then updating `g` at point `a` with value `b` using `Function.update`.
|
Mathlib.Data.Finsupp.Defs._auxLemma.3
theorem Mathlib.Data.Finsupp.Defs._auxLemma.3 :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M}, (f.support = ∅) = (f = 0)
This theorem, named `Mathlib.Data.Finsupp.Defs._auxLemma.3`, states that for any type `α` and any type `M` equipped with a zero element, and given a function `f` from `α` to `M` with finite support (`f : α →₀ M`), the support of `f` being empty (i.e., `f` has no non-zero outputs) is equivalent to `f` being the zero function (i.e., `f` outputs zero for all inputs). In mathematical terms, for a function with finite support, it having no non-zero outputs (or `f.support = ∅`) is the same as it being the zero function (or `f = 0`).
More concisely: A function with finite support from a type to a type equipped with a zero element is the zero function if and only if it has no non-zero outputs.
|
Finsupp.unique_ext
theorem Finsupp.unique_ext :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : Unique α] {f g : α →₀ M}, f default = g default → f = g
This theorem, `Finsupp.unique_ext`, asserts that for any two functions `f` and `g` from a type `α` to a type `M` with a zero element, if `α` is a unique type (i.e., there exists exactly one element of `α`) and the default values of `f` and `g` are equal, then the functions `f` and `g` are equal. The theorem essentially states that two functions on a unique type are equal if they agree on the value of the unique element.
More concisely: Given types `α` with exactly one element and `M` with a zero element, if two functions `f` and `g` from `α` to `M` have equal values at the unique element, then `f` and `g` are equal.
|
Finsupp.support_eq_empty
theorem Finsupp.support_eq_empty :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M}, f.support = ∅ ↔ f = 0
This theorem, `Finsupp.support_eq_empty`, declares a property for a function `f` of type `Finsupp` (which stands for "finite support"). Here, `Finsupp` is a type representing a function from `α` to `M` with finite support, i.e., there are only a finite number of elements of `α` for which `f` is non-zero. The theorem states that the support of `f` is empty if and only if `f` is the zero function. In other words, `f` maps all elements to zero if and only if there are no elements where `f` is non-zero. The `Zero M` instance indicates that `M` is a type with a specified zero element, and `∅` denotes an empty set.
More concisely: A function `f` of type `Finsupp α M` has an empty support if and only if it is the zero function.
|
Finsupp.support_onFinset_subset
theorem Finsupp.support_onFinset_subset :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {s : Finset α} {f : α → M} {hf : ∀ (a : α), f a ≠ 0 → a ∈ s},
(Finsupp.onFinset s f hf).support ⊆ s
The theorem `Finsupp.support_onFinset_subset` states that for any type `α`, any type `M` with a zero element, any finite set `s` of elements of type `α`, and any function `f` from `α` to `M` with the property that `f` is zero outside of `s`, the support of the `Finsupp` function produced by `Finsupp.onFinset` applied to `s`, `f`, and the mentioned property, is a subset of `s`. In simpler terms, the theorem tells us that the set of nonzero elements in the `Finsupp` representation created from a function restricted to a finite set is always a subset of the original finite set.
More concisely: For any finite set `s` and function `f` from a type `α` to a type `M` with a zero element, the support of the `Finsupp` function produced from `s`, `f`, and `f` being zero outside of `s`, is contained in `s`.
|
Finsupp.addHom_ext
theorem Finsupp.addHom_ext :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
⦃f g : (α →₀ M) →+ N⦄, (∀ (x : α) (y : M), (f fun₀ | x => y) = g fun₀ | x => y) → f = g
This theorem states that if two additive homomorphisms, from the function space `α →₀ M` to `N`, behave the same way on each function `single a b` (where `a` is an element from `α` and `b` is an element from `M`), then those two homomorphisms are equal. Here, `α →₀ M` denotes the function space of functions from `α` to `M` that are finitely supported, i.e., all but a finite number of their values are zero. And `single a b` represents a function in this space that takes the value `b` at `a` and zero elsewhere. "Additive homomorphisms" are functions that preserve the addition operation, and `AddZeroClass` is a typeclass for types having addition and zero operations.
More concisely: If two additive homomorphisms from the finitely supported function space `α →₀ M` to `N` agree on all functions `single a b`, then they are equal.
|
Finsupp.single_eq_of_ne
theorem Finsupp.single_eq_of_ne :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {b : M}, a ≠ a' → (fun₀ | a => b) a' = 0
This theorem states that for any types `α` and `M` (with `M` having a `Zero` instance), given elements `a` and `a'` of type `α`, and an element `b` of type `M`, if `a` is not equal to `a'`, then the value of the function `fun₀` (which maps `a` to `b`) at `a'` is zero. Essentially, this is saying that a function defined for a particular input will yield zero when evaluated at a different input.
More concisely: For any types `α` and `M` with a `Zero` instance, if `a ≠ a'` are elements of `α`, then `fun₀ a' = 0` where `fun₀ : α → M`.
|
Finsupp.coe_sub
theorem Finsupp.coe_sub :
∀ {α : Type u_1} {G : Type u_9} [inst : SubNegZeroMonoid G] (g₁ g₂ : α →₀ G), ⇑(g₁ - g₂) = ⇑g₁ - ⇑g₂
This theorem states that for any two `g₁` and `g₂`, which are finitely supported functions from a type `α` to a type `G` (where `G` is a subtraction and negation zero monoid), the function obtained by subtracting `g₂` from `g₁` is the same as subtracting the function `g₂` from the function `g₁`. In simpler words, the subtraction operation on finitely supported functions corresponds to pointwise subtraction of the functions.
More concisely: For any two finitely supported functions `g₁` and `g₂` from type `α` to a subtraction and negation zero monoid `G`, `g₁ - g₂` equals `g₁ - g₂` pointwise.
|
Finsupp.erase_same
theorem Finsupp.erase_same :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {f : α →₀ M}, (Finsupp.erase a f) a = 0
The theorem `Finsupp.erase_same` asserts that for any type `α`, for any type `M` equipped with a zero element, for any element `a` of type `α`, and any finitely supported function `f` from `α` to `M`, applying the function `Finsupp.erase a f` to the argument `a` will yield the zero element of `M`. In other words, if we erase the value at `a` in `f`, we get zero when we look up `a`.
More concisely: For any type `α` and type `M` with zero element, given an element `a` of type `α` and a finitely supported function `f` from `α` to `M`, `Finsupp.erase a f a = 0`.
|
Finsupp.support_mapRange
theorem Finsupp.support_mapRange :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} [inst : Zero M] [inst_1 : Zero N] {f : M → N} {hf : f 0 = 0}
{g : α →₀ M}, (Finsupp.mapRange f hf g).support ⊆ g.support
This theorem states that for any types `α`, `M`, and `N`, and for any function `f : M → N` that maps zero to zero, and any function `g : α →₀ M` (which is a function from `α` to `M` with finite support; in other words, `g` is zero for all but finitely many elements of `α`), the support of the result of mapping the range of `g` using `f` is a subset of the support of `g`. This essentially means that applying `f` to the range of `g` doesn't introduce any new non-zero values. The "support" of a function is the set of points where the function is non-zero.
More concisely: For functions `f : M → N` mapping zero to zero, `g : α →₀ M` with finite support, the support of `f ∘ g` is contained in the support of `g`.
|
Finsupp.induction
theorem Finsupp.induction :
∀ {α : Type u_1} {M : Type u_5} [inst : AddZeroClass M] {p : (α →₀ M) → Prop} (f : α →₀ M),
p 0 → (∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p ((fun₀ | a => b) + f)) → p f
This theorem, `Finsupp.induction`, states that for any type `α`, any type `M` that is an instance of the `AddZeroClass`, and any property `p` of functions from `α` to `M`, if `p` holds for the zero function and `p` holds for any function `f` plus a function that is zero everywhere except possibly at a single point `a` with value `b`, where `a` is not in the support of `f` and `b` is not zero, then `p` holds for any such function `f`. This is an induction principle for functions with finite support.
More concisely: If `α` is a type, `M` is an AddZeroClass, `p` is a property of functions from `α` to `M`, and `p` holds for the zero function and for any function `f` with finite support such that `p` holds for `f` and the function zero everywhere except possibly at a point `a` not in the support of `f` with value `b` not equal to zero, then `p` holds for `f`.
|
Finsupp.zero_apply
theorem Finsupp.zero_apply : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α}, 0 a = 0
This theorem states that for all type `α` and another type `M` that has a zero element (as indicated by the `Zero M` typeclass), and for any element `a` of type `α`, applying the function `0` to `a` yields the zero of type `M`. This is a property of the `Finsupp` or "finite support" function, which is defined such that it is zero for all but a finite number of elements.
More concisely: For any type `α` and type `M` with a zero element, and for any element `a` of type `α`, the application of the function `0` to `a` equals the zero element of type `M` in the `Finsupp` function.
|
Finsupp.mapRange_comp
theorem Finsupp.mapRange_comp :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P]
(f : N → P) (hf : f 0 = 0) (f₂ : M → N) (hf₂ : f₂ 0 = 0) (h : (f ∘ f₂) 0 = 0) (g : α →₀ M),
Finsupp.mapRange (f ∘ f₂) h g = Finsupp.mapRange f hf (Finsupp.mapRange f₂ hf₂ g)
The theorem `Finsupp.mapRange_comp` states that for any three types `α`, `M`, `N`, and `P`, given two functions `f : N → P` and `f₂ : M → N` that map zero to zero, and a function `g : α →₀ M` (which is a finitely supported function from `α` to `M`), mapping the range of `g` using the composition of `f` and `f₂` is equal to first mapping the range of `g` using `f₂` and then mapping the range of the result using `f`. This theorem illustrates the distributivity of the `mapRange` operation over function composition in the context of finitely supported functions.
More concisely: For any types `α`, `M`, `N`, and `P`, and finite support functions `g : α →₀ M` and `f : N → P`, `f ∘ f₂ ∘ g = f₂ ∘ g` whenever `f` and `f₂` map zero to zero.
|
Finsupp.single_left_inj
theorem Finsupp.single_left_inj :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {b : M},
b ≠ 0 → (((fun₀ | a => b) = fun₀ | a' => b) ↔ a = a')
This theorem, `Finsupp.single_left_inj`, states that for any types `α` and `M`, given a zero instance for `M` and given any `a`, `a'` from `α` and `b` from `M` where `b` is not equal to zero, the function `fun₀ | a => b` equals to `fun₀ | a' => b` if and only if `a` equals to `a'`. The function `fun₀ | a => b` here can be interpreted as a function that gives `b` when supplied `a` and gives zero otherwise. The theorem essentially tells us that such a function is injective: two different inputs `a` and `a'` will give the same output (i.e., `b`) only if `a` and `a'` are actually the same.
More concisely: The function `fun₀ | a => b` is a bijection from `α` to `{x : α | x ≠ a}`, whenever `b ≠ 0`.
|
Finsupp.support_single_ne_zero
theorem Finsupp.support_single_ne_zero :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {b : M} (a : α), b ≠ 0 → (fun₀ | a => b).support = {a}
This theorem, `Finsupp.support_single_ne_zero`, states that for any types `α` and `M` with `M` having a zero element, given a non-zero element `b` of type `M` and an element `a` of type `α`, the support (set of indices with non-zero values) of the function from `α` to `M` that maps `a` to `b` and all other elements to zero, is the singleton set containing only `a`. In other words, only the index `a` has a non-zero value (`b`) in this function.
More concisely: Given a function from type `α` to type `M` with domain size one and image `{a ↔ b}`, where `M` has a zero element and `b ≠ 0`, the support of this function is the singleton set `{a}`.
|
Finsupp.support_add_eq
theorem Finsupp.support_add_eq :
∀ {α : Type u_1} {M : Type u_5} [inst : AddZeroClass M] [inst_1 : DecidableEq α] {g₁ g₂ : α →₀ M},
Disjoint g₁.support g₂.support → (g₁ + g₂).support = g₁.support ∪ g₂.support
This theorem states that for any two functions `g₁` and `g₂` that map elements from a general type `α` to an additive monoid `M` with a zero element and having a decidable equality, if the supports (the set of points where the function is nonzero) of these functions are disjoint (in the sense that any element that is less than or equal to both of the supports is less than or equal to the bottom element of the order), then the support of the sum of these functions is equal to the union of their individual supports. In simpler terms, if two functions are nonzero at different sets of points, the set of points where their sum is nonzero is just the combination of the points where the original functions were nonzero.
More concisely: If `g₁` and `g₂` are functions from a type `α` to an additive monoid `M` with decidable equality, and the supports of `g₁` and `g₂` are disjoint, then the support of `g₁ + g₂` is equal to the union of the supports of `g₁` and `g₂`.
|
Finsupp.mem_support_iff
theorem Finsupp.mem_support_iff :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {a : α}, a ∈ f.support ↔ f a ≠ 0
This theorem states that for any types `α` and `M` with `M` being a structure with a zero element, and for any function `f` from `α` to `M` and any element `a` of `α`, `a` is in the support of `f` if and only if the result of applying `f` to `a` is not zero. In other words, the support of `f` is the set of all elements `a` from `α` such that when `f` is applied to `a`, the result is nonzero.
More concisely: The support of a function `f` from type `α` to a structure `M` with zero element is equal to the set of elements `a` in `α` such that `f a ≠ 0`.
|
Finsupp.unique_single
theorem Finsupp.unique_single :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : Unique α] (x : α →₀ M), x = fun₀ | default => x default
The theorem `Finsupp.unique_single` states that for any type `α` and a type `M` with a zero element, provided that `α` is unique, for any function `x` from `α` to `M` that has finite support (`α →₀ M`), `x` can be represented as a function which maps all elements in `α` to the default value of `x`. In other words, if `α` has only one element, any function from `α` to `M` with finite support can only have one possible mapping, which is to map the single element in `α` to its default value in `M`.
More concisely: If `α` is a type with a unique element, then any function from `α` to a type `M` with a zero element and finite support maps the unique element in `α` to its default value in `M`.
|
Finsupp.single_eq_same
theorem Finsupp.single_eq_same :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M}, (fun₀ | a => b) a = b
The theorem `Finsupp.single_eq_same` asserts that for any types `α` and `M`, given a zero instance for `M`, and any elements `a` of type `α` and `b` of type `M`, the function `fun₀` that maps `a` to `b` when applied to `a` gives `b`. In other words, this theorem proves that a function mapping a single element to another element will return that second element when applied to the first.
More concisely: For any type `α` and type `M` with a zero instance, the function mapping a single element `a` of type `α` to an element `b` of type `M` equals `b`.
|
Finsupp.single_eq_pi_single
theorem Finsupp.single_eq_pi_single :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : DecidableEq α] (a : α) (b : M),
(⇑fun₀ | a => b) = Pi.single a b
The theorem `Finsupp.single_eq_pi_single` asserts that for any types `α` and `M` with `M` having an instance of `Zero` and `α` having decidable equality, for any element `a` of type `α` and any element `b` of type `M`, the function `fun₀` applied to `a` yielding `b` is equal to the function `Pi.single` applied to `a` and `b`. The function `Pi.single a b` is a function that maps `a` to `b` and every other element of the type `α` to zero. The function `fun₀ | a => b` is a function that only has a non-zero value at `a`, where it equals `b`. Hence, this theorem establishes the equivalence of these two functions that are defined differently but behave the same way.
More concisely: For any type `α` with decidable equality and any type `M` with `Zero`, the function `fun₀ a := b` is equal to the function `Pi.single a b` for all `a : α` and `b : M`.
|
Finsupp.fun_support_eq
theorem Finsupp.fun_support_eq :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M), Function.support ⇑f = ↑f.support
The theorem `Finsupp.fun_support_eq` states that for any type `α` and a type `M` with a zero element (denoted by `Zero M`), and for any function `f` from `α` to `M` that is finitely supported (denoted by `f : α →₀ M`), the support of the function `f` (represented as `Function.support ⇑f`) is exactly equal to the support of the `f` considered as a finitely supported function (denoted by `↑f.support`). In other words, the set of points `x` in type `α` such that `f(x)` is non-zero is the same whether we consider `f` as an ordinary function or as a finitely supported function.
More concisely: For any type `α` and type `M` with a zero element, and for any finitely supported function `f : α →₀ M`, the set of points in `α` where `f` is non-zero is equal to the support of `f` as both an ordinary function and as a finitely supported function.
|
Finsupp.mem_support_toFun
theorem Finsupp.mem_support_toFun :
∀ {α : Type u_13} {M : Type u_14} [inst : Zero M] (self : α →₀ M) (a : α), a ∈ self.support ↔ self.toFun a ≠ 0 := by
sorry
This theorem, `Finsupp.mem_support_toFun`, states that for any given `Finsupp` (which stands for "finite support" function) and an element `a` of the domain type `α`, `a` belongs to the support of the `Finsupp` if and only if the value of the function at `a` is not zero. In other words, the support of a `Finsupp` is exactly the set of all `a` in `α` such that the function `Finsupp` does not map `a` to zero. Here, `M` is an arbitrary type equipped with a zero element.
More concisely: The support of a `Finsupp` function equals the domain elements mapping to non-zero values.
|