English
The map f ↦ indicator s f is injective: if indicator s f = indicator s g, then f = g.
Русский
Отображение f ↦ indicator s f инъективно: если indicator s f = indicator s g, то f = g.
LaTeX
$$$\\text{Injective}(f \\mapsto \\operatorname{indicator}(s,f))$; i.e., if $\\operatorname{indicator}(s,f)=\\operatorname{indicator}(s,g)$ then $f=g$.$$
Lean4
theorem indicator_injective : Injective fun f : ∀ i ∈ s, α => indicator s f :=
by
intro a b h
ext i hi
rw [← indicator_of_mem hi a, ← indicator_of_mem hi b]
exact DFunLike.congr_fun h i