preAleph_lt_preAleph

Mathlib.SetTheory.Cardinal.Aleph

URI: https://scilib.ai/kg/mathlib#Cardinal.preAleph_lt_preAleph

English

preAleph is strictly increasing: if o1 < o2 then preAleph(o1) < preAleph(o2).

Русский

PreAleph строго возрастает: если o1 < o2, то preAleph(o1) < preAleph(o2).

LaTeX

$$$ \text{preAleph}(o_1) < \text{preAleph}(o_2) \iff o_1 < o_2 $$$

Lean4

theorem preAleph_lt_preAleph {o₁ o₂ : Ordinal} : preAleph o₁ < preAleph o₂ ↔ o₁ < o₂ :=
  preAleph.lt_iff_lt

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

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

Разделы

Аффилиация

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