Finsupp.support_indicator_subset
theorem Finsupp.support_indicator_subset :
∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α),
↑(Finsupp.indicator s f).support ⊆ ↑s
The theorem `Finsupp.support_indicator_subset` states that for any finset `s` and function `f` from elements of `s` to a type `α` (with zero element), the support of the `Finsupp.indicator` of `s` and `f` (which is a function from `ι` to `α` that is zero outside of `s`) is a subset of `s`. In other words, all the non-zero elements in the function created by `Finsupp.indicator` are in the original finset `s`.
More concisely: The support of the indicator function of a finset and a function from its elements to a type is contained in the finset.
|
Finsupp.indicator_of_mem
theorem Finsupp.indicator_of_mem :
∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] {s : Finset ι} {i : ι} (hi : i ∈ s) (f : (i : ι) → i ∈ s → α),
(Finsupp.indicator s f) i = f i hi
The theorem `Finsupp.indicator_of_mem` states that for any types `ι` and `α` where `α` has a zero element, any finite set `s` of type `ι`, any element `i` of type `ι` that is in `s`, and any function `f` from elements of `s` to `α`, then applying the function `Finsupp.indicator s f` to `i` yields the same result as applying `f` to `i` with membership proof `hi`. The function `Finsupp.indicator` is defined to create an element in the function space `ι →₀ α` from a finite set `s` and a function `f` defined on `s`, such that the application of this function to any `i` outside `s` is zero.
More concisely: For any finite set `s`, function `f` on `s`, and `i` in `s`, `Finsupp.indicator s f i = f i` holds in Lean 4, given `i` is a member of `s` with proof `hi`.
|