English
Given a finite set s ⊆ ι and a function f defined on s with values in α, the indicator map creates an element of ι →₀ α that equals f(i) on i ∈ s and 0 otherwise. This establishes a canonical way to realize partial functions as finsupps.
Русский
Для конечного множества s ⊆ ι и функции f на s взять индикатор, который даёт f(i) при i ∈ s и 0 иначе; это даёт каноническое представление частичных функций как finsupp.
LaTeX
$$$\\big(\\operatorname{indicator}(s,f)\\big)(i)=\\begin{cases} f(i) & i\\in s \\\\ 0 & i\\notin s\\end{cases},\\quad \\operatorname{supp}(\\operatorname{indicator}(s,f))\\subseteq s$$$
Lean4
/-- Create an element of `ι →₀ α` from a finset `s` and a function `f` defined on this finset. -/
def indicator (s : Finset ι) (f : ∀ i ∈ s, α) : ι →₀ α
where
toFun
i :=
haveI := Classical.decEq ι
if H : i ∈ s then f i H else 0
support :=
haveI := Classical.decEq α
({i | f i.1 i.2 ≠ 0} : Finset s).map (Embedding.subtype _)
mem_support_toFun i := by classical simp
