omega_strictMono

Mathlib.SetTheory.Cardinal.Aleph

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

English

omega is strictly monotone with respect to index; i.e., indices increase imply increasing omegas.

Русский

ω строго монотонна по индексу: при возрастании индекса значения ω возрастают.

LaTeX

$$$\forall a

Lean4

theorem omega_strictMono : StrictMono omega :=
  omega.strictMono

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

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

Разделы

Аффилиация

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