lfp_mem_range_lfpApprox — Mathlib

English

There exists a value a such that a is a fixed point of f and appears in the GFP approximation chain, implying the GFP is reached at some index.

Русский

Существует значение a, которое является точкой фиксации f и появляется в цепочке GFP-аппроксимаций, что означает достижение GFP на некотором индексе.

LaTeX

$$$ \\exists a\\ (a \\in \\mathrm{fixedPoints}(f) \\wedge a = \\mathrm{lfpApprox}(f,\\perp, i) ) $$$

Lean4

/-- Some approximation of the least fixed point starting from `⊥` is the least fixed point. -/
theorem lfp_mem_range_lfpApprox : f.lfp ∈ Set.range (lfpApprox f ⊥) :=
  by
  use ord <| succ #α
  exact lfpApprox_ord_eq_lfp f

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