rank_vonNeumann

Mathlib.SetTheory.ZFC.VonNeumann

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

← MathLib Explorer

English

For all o, rank(V_o) = o.

Русский

Для любого ординала o ранг V_o равен o.

LaTeX

$$$ \operatorname{rank}(V_o) = o $$$

Lean4

@[simp]
theorem rank_vonNeumann (o : Ordinal) : rank (V_ o) = o :=
  le_antisymm (by rw [← subset_vonNeumann]) <|
    le_of_forall_lt fun a ha ↦ rank_vonNeumann a ▸ rank_lt_of_mem (vonNeumann_mem_of_lt ha)
termination_by o

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

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

Разделы

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

Аффилиация

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