gfpApprox_add_one — Mathlib

English

If two GFP indices yield the same approximation, then all later GFPs equal that same value.

Русский

Если два индекса GFP дают одно и то же приближение, то все последующие GFP равны этому значению.

LaTeX

$$$ a < b \\wedge \\mathrm{gfpApprox}(f,x,a) = \\mathrm{gfpApprox}(f,x,b) \\Rightarrow \\forall c \\ge b, \\mathrm{gfpApprox}(f,x,c) = \\mathrm{gfpApprox}(f,x,b) $$$

Lean4

theorem gfpApprox_add_one (h : f x ≤ x) (a : Ordinal) : gfpApprox f x (a + 1) = f (gfpApprox f x a) :=
  lfpApprox_add_one f.dual x h a

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