iterate_omega0_opow_lt_epsilon0 — Mathlib

English

For every natural number n, the nth iterate of the map a ↦ ω^a at 0 is less than ε₀.

Русский

Для каждого натурального числа n суперятная итерация отображения a ↦ ω^a в точке 0 меньше ε₀.

LaTeX

$$$\forall n \in \mathbb{N},\ (\omega^a)^{[n]} 0 < \varepsilon_0$$$

Lean4

/-- `ω ^ ω ^ … ^ 0 < ε₀` -/
theorem iterate_omega0_opow_lt_epsilon0 (n : ℕ) : (fun a ↦ ω ^ a)^[n] 0 < ε₀ :=
  by
  rw [epsilon0_eq_nfp]
  apply iterate_lt_nfp (isNormal_opow one_lt_omega0).strictMono
  simp

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