coe_inj — Mathlib

English

Equality of the underlying sets determines Finset equality: (s1 : Set α) = s2.toSet ⇔ s1 = s2.

Русский

Равенство подлежащих множеств определяет равенство Finset: (s1 : Set α) = s2.toSet ⇔ s1 = s2.

LaTeX

$$$ (s_1 : Set \alpha) = s_2 ^{\mathrm{toSet}} \\iff s_1 = s_2 $$$

Lean4

@[simp, norm_cast]
theorem coe_inj {s₁ s₂ : Finset α} : (s₁ : Set α) = s₂ ↔ s₁ = s₂ :=
  Set.ext_iff.trans Finset.ext_iff.symm

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