English
The monotonicity of lfpApprox persists when varying the function, with a fixed x and a given ordinal level. This is captured by monotone behavior in f, preserving order of lfp approximations.
Русский
Монотонность lfpApprox сохраняется при изменении функции, фиксированного x и заданного ординального уровня; поведение сохраняется по отношению к f и порядку lfp-аппроксимаций.
LaTeX
$$$ \\forall f,g \\ (f \\le g) \\Rightarrow (\\mathrm{lfpApprox} (f) \\le \\mathrm{lfpApprox} (g)) $$$
Lean4
theorem lfpApprox_mono_mid : Monotone (lfpApprox f) :=
by
intro x₁ x₂ h 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,
forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
constructor
· exact le_sup_of_le_left h
· intro i' h_i'
apply le_sup_of_le_right
apply le_sSup_of_le
· use i'
· exact f.monotone (ih i' h_i')
