preOmega_lt_preOmega

Mathlib.SetTheory.Cardinal.Aleph

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

English

Order of preOmega is preserved by ordering of indices.

Русский

Порядок preOmega сохраняется в соответствии с порядком индексов.

LaTeX

$$$\mathrm{preOmega}(o_1) < \mathrm{preOmega}(o_2) \iff o_1 < o_2$$$

Lean4

theorem preOmega_lt_preOmega {o₁ o₂ : Ordinal} : preOmega o₁ < preOmega o₂ ↔ o₁ < o₂ :=
  preOmega.lt_iff_lt

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

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

Разделы

Аффилиация

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