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.

noncomputable 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.

Equations

• Finsupp.indicator s f = Finsupp.onFinset s (fun (i : ι) => if H : i ∈ s then f i H else 0) ⋯

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

theorem Finsupp.indicator_of_notMem {ι : Type u_1} {α : Type u_2} [Zero α] {s : Finset ι} {i : ι} (hi : i ∉ s) (f : (i : ι) → i ∈ s → α) : (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 ι] : (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 : (i : ι) → i ∈ s → α) => indicator s f

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

theorem Finsupp.indicator_singleton {ι : Type u_1} {α : Type u_2} [Zero α] (a : ι) (f : (j : ι) → j ∈ {a} → α) : indicator {a} f = single a (f a ⋯)

@[deprecated Finsupp.indicator_singleton (since := "2026-04-27")]

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

theorem Finsupp.indicator_eq_set_indicator {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) (g : ι → α) : ⇑(indicator s fun (i : ι) (x : i ∈ s) => g i) = (↑s).indicator g

theorem Finsupp.indicator_indicator {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) {t : Finset ι} (f : (i : ι) → i ∈ s → α) [DecidableEq ι] : (indicator t fun (i : ι) (x : i ∈ t) => (indicator s f) i) = indicator (s ∩ t) fun (i : ι) (hi : i ∈ s ∩ t) => f i ⋯

theorem Finsupp.eq_indicator_iff {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α) {g : ι → α} : g = ⇑(indicator s f) ↔ Function.support g ⊆ ↑s ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i

theorem Finsupp.eq_indicator_self_iff {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) {d : ι →₀ α} : (d = indicator s fun (i : ι) (x : i ∈ s) => d i) ↔ d.support ⊆ s