mem_vonNeumann'

Mathlib.SetTheory.ZFC.VonNeumann

URI: https://scilib.ai/kg/mathlib#ZFSet.mem_vonNeumann'

English

For ordinal o and ZFSet x, x ∈ V_o if and only if there exists a < o with x ⊆ V_a.

Русский

Пусть o – ординал, x – ZFSet. Тогда x ∈ V_o тогда и только тогда, когда существует a < o такой, что x ⊆ V_a.

LaTeX

$$$$ x \in V_{o} \iff \exists a < o,\ x \subseteq V_{a} $$$$

Lean4

theorem mem_vonNeumann' : x ∈ V_ o ↔ ∃ a < o, x ⊆ V_ a := by rw [vonNeumann]; simp

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

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

Разделы

Аффилиация

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