gfpApprox_eq_of_mem_fixedPoints — Mathlib

English

If GFP approximations at a and b are equal and both are fixed points, then the GFP is stabilized at that fixed point for larger indices.

Русский

Если аппроксимации GFP в a и b равны и оба являются фиксированными точками, то GFP стабилизируется на этой точке для больших индексов.

LaTeX

$$$ a \\,\\text{and}\\, b \\text{ fixed points},\\; a < b \\Rightarrow \\mathrm{gfpApprox}(f,x,a) = \\mathrm{gfpApprox}(f,x,b) \\Rightarrow \\mathrm{gfpApprox}(f,x,c) = \\mathrm{gfpApprox}(f,x,b) \\ (c \\ge b) $$$

Lean4

/-- The approximations of the greatest fixed point stabilize at a fixed point of `f` -/
theorem gfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : f x ≤ x) (h_ab : a ≤ b)
    (h : gfpApprox f x a ∈ fixedPoints f) : gfpApprox f x b = gfpApprox f x a :=
  lfpApprox_eq_of_mem_fixedPoints f.dual x h_init h_ab h

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