iUnion_vonNeumann

Mathlib.SetTheory.ZFC.VonNeumann

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

English

The union over all o of V_o equals the universe.

Русский

Объединение по всем o от V_o дает вселенную.

LaTeX

$$$ \bigcup o\, V_o = \mathsf{Class.univ} $$$

Lean4

theorem iUnion_vonNeumann : ⋃ o, (V_ o : Class) = Class.univ :=
  Class.eq_univ_of_forall fun x ↦ Set.mem_iUnion.2 <| exists_mem_vonNeumann x

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

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

Разделы

Аффилиация

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