ext — Mathlib

English

If two sets have exactly the same elements, then they are equal.

Русский

Если два множества содержат одни и те же элементы, то они равны.

LaTeX

$$$\forall x,y : ZFSet, (\forall z : ZFSet, z \in x \leftrightarrow z \in y) \rightarrow x = y$$$

Lean4

@[ext]
theorem ext {x y : ZFSet.{u}} : (∀ z : ZFSet.{u}, z ∈ x ↔ z ∈ y) → x = y :=
  Quotient.inductionOn₂ x y fun _ _ h => Quotient.sound (Mem.ext fun w => h ⟦w⟧)

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