iSup_iterate_eq_nfp — Mathlib

English

The supremum over all iterates of f at a equals the least fixed point of f at a: ⨆ n, f^[n] a = nfp f a.

Русский

supremum всех итераций f в a равен наименьшей фиксированной точке f в a: ⨆ n, f^[n] a = nfp f a.

LaTeX

$$$$ \big\lVert_{n \in \mathbb{N}} f^{[n]} a = nfp f a. $$$$

Lean4

theorem iSup_iterate_eq_nfp (f : Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}) : ⨆ n : ℕ, f^[n] a = nfp f a :=
  by
  apply le_antisymm
  · rw [Ordinal.iSup_le_iff]
    intro n
    rw [← List.length_replicate (n := n) (a := Unit.unit), ← List.foldr_const f a]
    exact Ordinal.le_iSup _ _
  · apply Ordinal.iSup_le
    intro l
    rw [List.foldr_const f a l]
    exact Ordinal.le_iSup _ _

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