isSuccLimit_opow_left — Mathlib

English

If a is a succ-limit and b ≠ 0, then IsSuccLimit(a^b).

Русский

Если a является предельным стремительным пределом и b ≠ 0, то IsSuccLimit(a^b).

LaTeX

$$$\forall a,b : \mathrm{Ordinal},\ \mathrm{IsSuccLimit}(a) \land b \neq 0 \Rightarrow \mathrm{IsSuccLimit}(a^b)$$$

Lean4

theorem isSuccLimit_opow_left {a b : Ordinal} (l : IsSuccLimit a) (hb : b ≠ 0) : IsSuccLimit (a ^ b) :=
  by
  rcases zero_or_succ_or_isSuccLimit b with (e | ⟨b, rfl⟩ | l')
  · exact absurd e hb
  · rw [opow_succ]
    exact isSuccLimit_mul (opow_pos _ l.bot_lt) l
  · exact isSuccLimit_opow (one_lt_of_isSuccLimit l) l'

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