indicator_injective — Mathlib

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

Похожие утверждения