English
If x ≤ f x, the lfpApprox at a+1 is the image of the lfpApprox at a under f, formalizing the step-by-step construction of the least fixed point.
Русский
Если x ≤ f x, аппроксимация lfp на шаге a+1 равна образу lfp(a) под действием f, что формализует пошаговую конструкцию наименьшей фиксированной точки.
LaTeX
$$$ (x \\le f x) \\rightarrow (\\mathrm{lfpApprox}\, f\, x\, (a+1) = f(\\mathrm{lfpApprox}\, f\, x\, a)) $$$
Lean4
theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) : lfpApprox f x (a + 1) = f (lfpApprox f x a) :=
by
apply le_antisymm
· conv => left; rw [lfpApprox]
apply sSup_le
simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop, Set.union_singleton, Set.mem_insert_iff,
Set.mem_setOf_eq, forall_eq_or_imp, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
apply And.intro
· apply le_trans h
apply Monotone.imp f.monotone
exact le_lfpApprox f x
· intro a' h
apply f.2; apply lfpApprox_monotone; exact h
· conv => right; rw [lfpApprox]
apply le_sSup
simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop]
rw [Set.mem_union]
apply Or.inl
simp only [Set.mem_setOf_eq]
use a
