English
The function lfpApprox is monotone in its first argument, i.e., increasing the operator f preserves the order of the approximations.
Русский
Функция lfpApprox монотонна по первому аргументу: если порядок увеличивается, аппроксимации не уменьшаются.
LaTeX
$$$ \\text{Monotone}(\\mathrm{lfpApprox}: (\\alpha \\to \\alpha) \\to (\\alpha) \\to \\alpha) $$$
Lean4
theorem lfpApprox_mono_left : Monotone (lfpApprox : (α →o α) → _) :=
by
intro f g h x a
induction a using Ordinal.induction with
| h i ih =>
rw [lfpApprox, lfpApprox]
apply sSup_le
simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, sSup_insert, forall_eq_or_imp,
le_sup_left, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, true_and]
intro i' h_lt
apply le_sup_of_le_right
apply le_sSup_of_le
· use i'
· apply le_trans (h _)
simp only [OrderHom.toFun_eq_coe]
exact g.monotone (ih i' h_lt)
