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.

Instances For

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 → α) :

theorem Finsupp.indicator_singleton {ι : Type u_1} {α : Type u_2} [Zero α] (a : ι) (f : (j : ι) → j ∈ {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