English
If f is ω-Scott-continuous, then the least fixed point of f equals the supremum of the iterates of f applied to the bottom element: lfp(f) = sup_{n≥0} f^n(⊥).
Русский
Если f — ω-Scott непрерывно, то наименьшая фиксированная точка f равна сверху по всем итерациям: lfp(f) = sup_{n≥0} f^n(⊥).
LaTeX
$$$$\\mathrm{lfp}(f) = \\bigvee_{n \\ge 0} f^{[n]}(\\bot)$$$$
Lean4
/-- **Kleene's fixed point Theorem**: The least fixed point in a complete lattice is
the supremum of iterating a function on bottom arbitrary often. -/
theorem lfp_eq_sSup_iterate (h : ωScottContinuous f) : f.lfp = ⨆ n, f^[n] ⊥ :=
by
apply le_antisymm
· apply lfp_le_fixed
exact Function.mem_fixedPoints.mp (ωSup_iterate_mem_fixedPoint ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le)
· apply le_lfp
intro a h_a
exact ωSup_iterate_le_prefixedPoint ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le h_a bot_le
