range_preOmega

Mathlib.SetTheory.Cardinal.Aleph

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

English

The range of preOmega equals the set of initial ordinals.

Русский

Область значений preOmega равна множеству начальных ординалов.

LaTeX

$$$\mathrm{range}(\mathrm{preOmega}) = \{ x \mid \mathrm{IsInitial}(x) \}$$$

Lean4

@[simp]
theorem range_preOmega : range preOmega = {x | IsInitial x} :=
  range_enumOrd not_bddAbove_isInitial

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

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

Разделы

Аффилиация

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