omega0_lt_preOmega_iff

Mathlib.SetTheory.Cardinal.Aleph

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

English

ω0 < preOmega x if and only if ω0 < x.

Русский

ω0 < preOmega x равно ω0 < x.

LaTeX

$$$\omega_0 < \mathrm{preOmega}(x) \iff \omega_0 < x$$$

Lean4

@[simp]
theorem omega0_lt_preOmega_iff {x : Ordinal} : ω < preOmega x ↔ ω < x := by
  conv_lhs => rw [← preOmega_omega0, preOmega_lt_preOmega]

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

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

Разделы

Аффилиация

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