Building finitely supported functions off finsets

This file defines Finsupp.indicator to help create finsupps from finsets.

Main declarations

• Finsupp.indicator: Turns a map from a Finset into a Finsupp from the entire type.

def Finsupp.indicator {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α) : ι →₀ α

Create an element of ι →₀ α from a finset s and a function f defined on this finset.

theorem Finsupp.indicator_of_mem {ι : Type u_1} {α : Type u_2} [Zero α] {s : Finset ι} {i : ι} (hi : i ∈ s) (f : (i : ι) → i ∈ s → α) : ↑(Finsupp.indicator s f) i = f i hi

theorem Finsupp.indicator_of_not_mem {ι : Type u_1} {α : Type u_2} [Zero α] {s : Finset ι} {i : ι} (hi : ¬i ∈ s) (f : (i : ι) → i ∈ s → α) : ↑(Finsupp.indicator s f) i = 0

@[simp]

theorem Finsupp.indicator_apply {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α) (i : ι) [DecidableEq ι] : ↑(Finsupp.indicator s f) i = if hi : i ∈ s then f i hi else 0

theorem Finsupp.indicator_injective {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) : Function.Injective fun f => Finsupp.indicator s f

theorem Finsupp.support_indicator_subset {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α) : ↑(Finsupp.indicator s f).support ⊆ ↑s

theorem Finsupp.single_eq_indicator {ι : Type u_1} {α : Type u_2} [Zero α] (i : ι) (b : α) : Finsupp.single i b = Finsupp.indicator {i} fun x x => b