gfp_eq_sInf_iterate — Mathlib

English

Dually to lfp, if f is ω-Scott-continuous in the dual sense, the greatest fixed point equals the infimum of iterates from the top: gfp(f) = inf_{n≥0} f^n(⊤).

Русский

Дуально к lfp, если применимый к двойственному образованию f обладает ω-Scott непрерывностью, тогда наибольшая фиксированная точка равна инфимума всем итерациям из верха: gfp(f) = inf_{n≥0} f^n(⊤).

LaTeX

$$$$\\mathrm{gfp}(f) = \\bigwedge_{n \\ge 0} f^{[n]}(\\top)$$$$

Lean4

theorem gfp_eq_sInf_iterate (h : ωScottContinuous f.dual) : f.gfp = ⨅ n, f^[n] ⊤ :=
  lfp_eq_sSup_iterate f.dual h

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