English
Every value of the lfpApprox is bounded above by any fixed point of f that is above the initial value x, with the bound holding for all ordinal indices i.
Русский
Любое значение lfpApprox ограничено сверху фиксированной точкой f выше начального значения x и эта грань держится для всех индексов по ординалам.
LaTeX
$$$ \\forall a \\in fixedPoints\\, f,\; x \\le a \\rightarrow \\forall i, \\mathrm{lfpApprox}\, f\, x\, i \\le a $$$
Lean4
/-- Every value of the approximation is less or equal than every fixed point of `f`
greater or equal than the initial value -/
theorem lfpApprox_le_of_mem_fixedPoints {a : α} (h_a : a ∈ fixedPoints f) (h_le_init : x ≤ a) (i : Ordinal) :
lfpApprox f x i ≤ a := by
induction i using Ordinal.induction with
| h i IH =>
rw [lfpApprox]
apply sSup_le
simp only [exists_prop]
intro y h_y
simp only [Set.mem_union, Set.mem_setOf_eq, Set.mem_singleton_iff] at h_y
cases h_y with
| inl h_y =>
let ⟨j, h_j_lt, h_j⟩ := h_y
rw [← h_j, ← h_a]
exact f.monotone' (IH j h_j_lt)
| inr h_y =>
rw [h_y]
exact h_le_init
