mem_vonNeumann

Mathlib.SetTheory.ZFC.VonNeumann

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

← MathLib Explorer

English

Let o be an ordinal and x a ZF set. Then x ∈ V_o iff rank x < o.

Русский

Пусть o — ординал, x — множество. Тогда x ∈ V_o эквивалентно rank(x) < o.

LaTeX

$$$ x \in V_o \iff \operatorname{rank}(x) < o $$$

Lean4

theorem mem_vonNeumann : x ∈ V_ o ↔ rank x < o :=
  by
  simp_rw [mem_vonNeumann', subset_vonNeumann]
  exact ⟨fun ⟨a, h₁, h₂⟩ ↦ h₂.trans_lt h₁, by aesop⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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