English
For a monotone f on a complete lattice and x ≤ f(x), nextFixed(x) is the least fixed point of f that is at least x.
Русский
Для монотонной f на полной решетке, если x ≤ f(x), то nextFixed(x) — наименьшая фиксированная точка, не меньшая чем x.
LaTeX
$$$\text{nextFixed}(x, hx) = \min\{y \mid f(y)=y, x \le y\}$.$$
Lean4
/-- Next fixed point of a monotone map. If `f` is a monotone self-map of a complete lattice and
`x` is a point such that `x ≤ f x`, then `f.nextFixed x hx` is the least fixed point of `f`
that is greater than or equal to `x`. -/
def nextFixed (x : α) (hx : x ≤ f x) : fixedPoints f :=
{ f.dual.prevFixed x hx with val := (const α x ⊔ f).lfp }
