coe_inj — Mathlib

English

For Sym α n, the injectivity of the coe equality: (s1.toMultiset = s2.toMultiset) ⇔ (s1 = s2).

Русский

Для Sym α n справедливо: (s1.toMultiset = s2.toMultiset) ⇔ (s1 = s2).

LaTeX

$$$ (s_1 : \\mathrm{Sym}\\;\\alpha\\;n) \\,.toMultiset = (s_2 : \\mathrm{Sym}\\;\\alpha\\;n) \\;\\Longleftrightarrow\\; s_1 = s_2 $$$

Lean4

@[simp, norm_cast]
theorem coe_inj {s₁ s₂ : Sym α n} : (s₁ : Multiset α) = s₂ ↔ s₁ = s₂ :=
  coe_injective.eq_iff

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