Theorems · Definition · order theory

OrderHom.nextFixed

{α : Type u} → [inst : CompleteLattice α] → (f : α →o α) → (x : α) → x ≤ f x → ↑(Function.fixedPoints ⇑f)

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.

Defined in

Mathlib.Order.FixedPoints

Cited by

4 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

CompleteLattice