opow_pos — Mathlib

English

If a > 0, then a^b > 0 for all ordinals b.

Русский

Если a > 0, то для любого ординала b выполняется a^b > 0.

LaTeX

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

Lean4

theorem opow_pos {a : Ordinal} (b : Ordinal) (a0 : 0 < a) : 0 < a ^ b :=
  by
  have h0 : 0 < a ^ (0 : Ordinal) := by simp only [opow_zero, zero_lt_one]
  induction b using limitRecOn with
  | zero => exact h0
  | succ b IH =>
    rw [opow_succ]
    exact mul_pos IH a0
  | limit b l _ => exact (lt_opow_of_isSuccLimit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.bot_lt, h0⟩

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