le_gfpApprox_of_mem_fixedPoints — Mathlib

English

The GFP approximation converges to the greatest fixed point as the index tends to the top of the lattice.

Русский

Аппроксимация GFP сходится к наибольшей фиксированной точке по мере роста индекса к верхней границе решётки.

LaTeX

$$$ \\lim_{i \\to \\operatorname{ord}} \\mathrm{gfpApprox}(f,x,i) = f\\,\\mathrm{gfp} $$$

Lean4

/-- Every value of the approximation is greater or equal than every fixed point of `f`
less or equal than the initial value -/
theorem le_gfpApprox_of_mem_fixedPoints {a : α} (h_a : a ∈ fixedPoints f) (h_le_init : a ≤ x) (i : Ordinal) :
    a ≤ gfpApprox f x i :=
  lfpApprox_le_of_mem_fixedPoints f.dual x h_a h_le_init i

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