English
For a monotone f on a complete lattice, prevFixed(x) is the greatest fixed point not exceeding x, given a proof f(x) ≤ x.
Русский
Для монотонной f на полной решетке prevFixed(x) — наибольшая фиксированная точка, не превосходящая x.
LaTeX
$$$\text{prevFixed}(x, hx) = \text{the greatest fixed point of } f \text{ with } ≤ x$.$$
Lean4
/-- Previous fixed point of a monotone map. If `f` is a monotone self-map of a complete lattice and
`x` is a point such that `f x ≤ x`, then `f.prevFixed x hx` is the greatest fixed point of `f`
that is less than or equal to `x`. -/
def prevFixed (x : α) (hx : f x ≤ x) : fixedPoints f :=
⟨(const α x ⊓ f).gfp,
calc
f (const α x ⊓ f).gfp = x ⊓ f (const α x ⊓ f).gfp :=
Eq.symm <| inf_of_le_right <| (f.mono <| f.gfp_const_inf_le x).trans hx
_ = (const α x ⊓ f).gfp := (const α x ⊓ f).map_gfp⟩
