opow_lt_opow_left_of_succ — Mathlib

English

If a < b are ordinals, then a^{succ c} < b^{succ c} for any ordinal c.

Русский

Пусть a и b — ординалы и a < b. Тогда a^{succ c} < b^{succ c} для любого c.

LaTeX

$$$\forall a,b,c \in \mathrm{Ordinal},\ a < b \Rightarrow a^{\operatorname{succ} c} < b^{\operatorname{succ} c}$$$

Lean4

theorem opow_lt_opow_left_of_succ {a b c : Ordinal} (ab : a < b) : a ^ succ c < b ^ succ c :=
  by
  rw [opow_succ, opow_succ]
  exact
    (mul_le_mul_right' (opow_le_opow_left c ab.le) a).trans_lt <|
      mul_lt_mul_of_pos_left ab <| opow_pos c <| (Ordinal.zero_le a).trans_lt ab

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