gfp_mem_range_gfpApprox — Mathlib

English

Let α be a complete lattice and f: α → α an order-preserving endomorphism. Then the greatest fixed point f.gfp is in the image of the approximants gfpApprox f starting from the top, i.e. f.gfp ∈ Range(gfpApprox f ⊤).

Русский

Пусть α — полная решетка и f: α → α монотонное отображение α в α. Тогда наибольшая точка фиксации f.gfp принадлежит образу приближений фиксации gfpApprox f, взятому от верхней границы ⊤, то есть f.gfp ∈ Range(gfpApprox f ⊤).

LaTeX

$$$ f.\\mathrm{gfp} \\in \\operatorname{Range}(gfpApprox\, f\, \\top) $$$

Lean4

/-- Some approximation of the least fixed point starting from `⊤` is the greatest fixed point. -/
theorem gfp_mem_range_gfpApprox : f.gfp ∈ Set.range (gfpApprox f ⊤) :=
  lfp_mem_range_lfpApprox f.dual

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