toSet_inj

Mathlib.SetTheory.ZFC.Basic

URI: https://scilib.ai/kg/mathlib#ZFSet.toSet_inj

English

Two ZFSets have equal toSet representations if and only if the sets are equal.

Русский

Два ZFSet равны по toSet тогда и только тогда, когда сами множества равны.

LaTeX

$$$\forall {x y : ZFSet}, x.toSet = y.toSet \iff x = y$$$

Lean4

@[simp]
theorem toSet_inj {x y : ZFSet} : x.toSet = y.toSet ↔ x = y :=
  toSet_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru