ext — Mathlib

English

Finite sets s1 and s2 are equal if and only if every element belongs to both: ∀ a, a ∈ s1 ↔ a ∈ s2.

Русский

Два конечных множества равны тогда и только тогда, когда каждый элемент принадлежит каждому из них: ∀ a, a ∈ s1 ↔ a ∈ s2.

LaTeX

$$$ \forall s_1 s_2 : \mathrm{Finset} \alpha, \left( \forall a, a \in s_1 \leftrightarrow a \in s_2 \right) \Rightarrow s_1 = s_2 $$$

Lean4

@[ext, grind ext]
theorem ext {s₁ s₂ : Finset α} (h : ∀ a, a ∈ s₁ ↔ a ∈ s₂) : s₁ = s₂ :=
  (val_inj.symm.trans <| s₁.nodup.ext s₂.nodup).mpr h

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