left_lt_opow

Mathlib.SetTheory.Ordinal.Exponential

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

English

If 1 < a and 1 < b, then a < a^b.

Русский

Если 1 < a и 1 < b, то a < a^b.

LaTeX

$$$\forall a,b : \mathrm{Ordinal},\ 1 < a \land 1 < b \Rightarrow a < a^b$$$

Lean4

theorem left_lt_opow {a b : Ordinal} (ha : 1 < a) (hb : 1 < b) : a < a ^ b :=
  by
  conv_lhs => rw [← opow_one a]
  rwa [opow_lt_opow_iff_right ha]

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

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

Разделы

Аффилиация

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