ext — Mathlib

English

Two classes are equal if and only if they assign the same membership to every ZFSet; i.e., they have the same elements.

Русский

Два класса равны тогда и только тогда, когда для каждого ZF-множества они устанавливают одинаковое членство; то есть они имеют одинаковые элементы.

LaTeX

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

Lean4

@[ext]
theorem ext {x y : Class.{u}} : (∀ z : ZFSet.{u}, x z ↔ y z) → x = y :=
  Set.ext

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