Building finitely supported functions off finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [has_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 = {support := finset.map (function.embedding.subtype (λ (x : ι), x ∈ s)) (finset.filter (λ (i : ↥s), f i.val _ ≠ 0) s.attach), to_fun := λ (i : ι), dite (i ∈ s) (λ (H : i ∈ s), f i H) (λ (H : i ∉ s), 0), mem_support_to_fun := _}

theorem finsupp.indicator_of_mem {ι : Type u_1} {α : Type u_2} [has_zero α] {s : finset ι} {i : ι} (hi : i ∈ s) (f : Π (i : ι), i ∈ s → α) :

theorem finsupp.indicator_of_not_mem {ι : Type u_1} {α : Type u_2} [has_zero α] {s : finset ι} {i : ι} (hi : i ∉ s) (f : Π (i : ι), i ∈ s → α) :

@[simp]

theorem finsupp.indicator_apply {ι : Type u_1} {α : Type u_2} [has_zero α] (s : finset ι) (f : Π (i : ι), i ∈ s → α) (i : ι) [decidable_eq ι] :

⇑(finsupp.indicator s f) i = dite (i ∈ s) (λ (hi : i ∈ s), f i hi) (λ (hi : i ∉ s), 0)

theorem finsupp.indicator_injective {ι : Type u_1} {α : Type u_2} [has_zero α] (s : finset ι) :

theorem finsupp.support_indicator_subset {ι : Type u_1} {α : Type u_2} [has_zero α] (s : finset ι) (f : Π (i : ι), i ∈ s → α) :

theorem finsupp.single_eq_indicator {ι : Type u_1} {α : Type u_2} [has_zero α] (i : ι) (b : α) :

finsupp.single i b = finsupp.indicator {i} (λ (_x : ι) (_x : _x ∈ {i}), b)