omega0_opow_mul_nat_lt

Mathlib.SetTheory.Ordinal.Exponential

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

← MathLib Explorer

English

log_b 1 = 0 for any base b.

Русский

log_b 1 = 0 для любого основания b.

LaTeX

$$$ \log_b 1 = 0 $$$

Lean4

theorem omega0_opow_mul_nat_lt {a b : Ordinal} (h : a < b) (n : ℕ) : ω ^ a * n < ω ^ b :=
  by
  apply lt_of_lt_of_le _ (opow_le_opow_right omega0_pos (succ_le_of_lt h))
  rw [opow_succ]
  gcongr
  exacts [opow_pos a omega0_pos, nat_lt_omega0 n]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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