vonNeumann_succ

Mathlib.SetTheory.ZFC.VonNeumann

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

← MathLib Explorer

English

V_(succ o) = powerset(V_o).

Русский

V_(succ o) = P(V_o).

LaTeX

$$$ V_{\operatorname{succ}(o)} = \mathcal{P}(V_o) $$$

Lean4

@[simp]
theorem vonNeumann_succ (o : Ordinal) : V_ (succ o) = powerset (V_ o) :=
  ext fun z ↦ by rw [mem_vonNeumann, mem_powerset, subset_vonNeumann, lt_succ_iff]

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

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

Разделы

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

Аффилиация

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