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 afinsetinto afinsuppfrom 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 → α) :
⇑(finsupp.indicator s f) i = f i hi
theorem
finsupp.indicator_of_not_mem
{ι : Type u_1}
{α : Type u_2}
[has_zero α]
{s : finset ι}
{i : ι}
(hi : i ∉ s)
(f : Π (i : ι), i ∈ s → α) :
⇑(finsupp.indicator s f) i = 0
theorem
finsupp.indicator_injective
{ι : Type u_1}
{α : Type u_2}
[has_zero α]
(s : finset ι) :
function.injective (λ (f : Π (i : ι), i ∈ s → α), finsupp.indicator s f)
theorem
finsupp.support_indicator_subset
{ι : Type u_1}
{α : Type u_2}
[has_zero α]
(s : finset ι)
(f : Π (i : ι), i ∈ s → α) :
↑((finsupp.indicator s f).support) ⊆ ↑s