exists_mem_vonNeumann

Mathlib.SetTheory.ZFC.VonNeumann

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

← MathLib Explorer

English

For every x there exists an ordinal o such that x ∈ V_o.

Русский

Для каждого x существует ординал o, такой что x ∈ V_o.

LaTeX

$$$ \exists o\, x \in V_o $$$

Lean4

/-- Every set is in some element of the von Neumann hierarchy. -/
theorem exists_mem_vonNeumann (x : ZFSet) : ∃ o, x ∈ V_ o :=
  ⟨_, mem_vonNeumann_succ x⟩

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

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

Разделы

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

Аффилиация

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