opow_le_opow_left — Mathlib

English

If a ≤ b, then a^c ≤ b^c.

Русский

Если a ≤ b, то a^c ≤ b^c.

LaTeX

$$$\forall a,b,c : \mathrm{Ordinal},\ \mathrm{le}\; a \; b \Rightarrow a^c \le b^c$$$

Lean4

theorem opow_le_opow_left {a b : Ordinal} (c : Ordinal) (ab : a ≤ b) : a ^ c ≤ b ^ c :=
  by
  by_cases ha : a = 0
  · by_cases c = 0 <;> simp_all
  ·
    induction c using limitRecOn with
    | zero => simp
    | succ c IH => simpa using mul_le_mul' IH ab
    | limit c l IH =>
      exact
        (opow_le_of_isSuccLimit ha l).2 fun b' h ↦
          (IH _ h).trans (opow_le_opow_right ((Ordinal.pos_iff_ne_zero.2 ha).trans_le ab) h.le)

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