# 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.
def Finsupp.indicator {ι : Type u_1} {α : Type u_2} [Zero α] (s : ) (f : (i : ι) → i sα) :
ι →₀ α

Create an element of ι →₀ α from a finset s and a function f defined on this finset.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Finsupp.indicator_of_mem {ι : Type u_1} {α : Type u_2} [Zero α] {s : } {i : ι} (hi : i s) (f : (i : ι) → i sα) :
() i = f i hi
theorem Finsupp.indicator_of_not_mem {ι : Type u_1} {α : Type u_2} [Zero α] {s : } {i : ι} (hi : is) (f : (i : ι) → i sα) :
() i = 0
@[simp]
theorem Finsupp.indicator_apply {ι : Type u_1} {α : Type u_2} [Zero α] (s : ) (f : (i : ι) → i sα) (i : ι) [] :
() i = if hi : i s then f i hi else 0
theorem Finsupp.indicator_injective {ι : Type u_1} {α : Type u_2} [Zero α] (s : ) :
Function.Injective fun (f : (i : ι) → i sα) =>
theorem Finsupp.support_indicator_subset {ι : Type u_1} {α : Type u_2} [Zero α] (s : ) (f : (i : ι) → i sα) :
().support s
theorem Finsupp.single_eq_indicator {ι : Type u_1} {α : Type u_2} [Zero α] (i : ι) (b : α) :
= Finsupp.indicator {i} fun (x : ι) (x : x {i}) => b