unsym_inj — Mathlib

English

The map unsym : SymAlg(α) → α is injective; equivalently, for all a,b ∈ SymAlg(α), unsym(a) = unsym(b) iff a = b.

Русский

Функция unsym : SymAlg(α) → α инъективна; то есть для любых a,b ∈ SymAlg(α) верно unsym(a) = unsym(b) ⇔ a = b.

LaTeX

$$$\forall a,b \in \operatorname{SymAlg}(\alpha),\ unsym(a) = unsym(b) \iff a=b$$$

Lean4

theorem unsym_inj {a b : αˢʸᵐ} : unsym a = unsym b ↔ a = b :=
  unsym_injective.eq_iff

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