gfpApprox_ord_mem_fixedPoint — Mathlib

English

For all f and x in a complete lattice, the GFP approximation as a function of the index a is monotone.

Русский

Для всех f и x в полной решётке GFP-аппроксимация как функция индекса a монотонна.

LaTeX

$$$ \\forall a,b \\ (a \\le b) \\Rightarrow \\mathrm{gfpApprox}(f,x,a) \\le \\mathrm{gfpApprox}(f,x,b) $$$

Lean4

/-- The approximation at the index of the successor of the domain's cardinality is a fixed point -/
theorem gfpApprox_ord_mem_fixedPoint (h_init : f x ≤ x) : gfpApprox f x (ord <| succ #α) ∈ fixedPoints f :=
  lfpApprox_ord_mem_fixedPoint f.dual x h_init

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