subset_vonNeumann_self

Mathlib.SetTheory.ZFC.VonNeumann

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

English

For every ZF set x, we have x ⊆ V_(rank x).

Русский

Для каждого множества ЗФ выполняется x ⊆ V_{rank(x)}.

LaTeX

$$$ x \subseteq V_{\operatorname{rank}(x)} $$$

Lean4

theorem subset_vonNeumann_self (x : ZFSet) : x ⊆ V_ (rank x) := by simp [subset_vonNeumann]

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

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

Разделы

Аффилиация

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