iSup_pow — Mathlib

English

If o > 0, then the supremum over n of o^n equals o^ω.

Русский

Пусть o > 0, тогда sup_n o^n = o^ω.

LaTeX

$$$ \big\lVert \sup_{n\in\mathbb{N}} o^n = o^\omega \big\rVert $$$

Lean4

theorem iSup_pow {o : Ordinal} (ho : 0 < o) : ⨆ n : ℕ, o ^ n = o ^ ω :=
  by
  simp_rw [← opow_natCast]
  rcases (one_le_iff_pos.2 ho).lt_or_eq with ho₁ | rfl
  · exact (isNormal_opow ho₁).apply_omega0
  · rw [one_opow]
    refine le_antisymm (Ordinal.iSup_le fun n => by rw [one_opow]) ?_
    exact_mod_cast Ordinal.le_iSup _ 0

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