vonNeumann_mem_vonNeumann_iff

Mathlib.SetTheory.ZFC.VonNeumann

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

English

For all a,b, V_a ∈ V_b iff a < b.

Русский

Для любых a,b: V_a ∈ V_b эквивалентно a < b.

LaTeX

$$$ V_a \in V_b \iff a < b $$$

Lean4

@[simp]
theorem vonNeumann_mem_vonNeumann_iff : V_ a ∈ V_ b ↔ a < b := by simp [mem_vonNeumann]

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

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

Разделы

Аффилиация

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