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 aFinset
into aFinsupp
from the entire type.
@[deprecated Finsupp.indicator_of_notMem (since := "2025-05-23")]
theorem
Finsupp.indicator_of_not_mem
{ι : Type u_1}
{α : Type u_2}
[Zero α]
{s : Finset ι}
{i : ι}
(hi : i ∉ s)
(f : (i : ι) → i ∈ s → α)
:
Alias of Finsupp.indicator_of_notMem
.
theorem
Finsupp.indicator_injective
{ι : Type u_1}
{α : Type u_2}
[Zero α]
(s : Finset ι)
:
Function.Injective fun (f : (i : ι) → i ∈ s → α) => indicator s f