mem_range_preOmega_iff

Mathlib.SetTheory.Cardinal.Aleph

URI: https://scilib.ai/kg/mathlib#Ordinal.mem_range_preOmega_iff

English

An ordinal x belongs to the range of preOmega iff x is initial.

Русский

Ординал x принадлежит диапазону preOmega тогда и только тогда, когда x начальный.

LaTeX

$$$x \in \mathrm{range}(\mathrm{preOmega}) \iff \mathrm{IsInitial}(x)$$$

Lean4

theorem mem_range_preOmega_iff {x : Ordinal} : x ∈ range preOmega ↔ IsInitial x := by rw [range_preOmega, mem_setOf]

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

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

Разделы

Аффилиация

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