# mathlib3documentation

order.fixed_points

# Fixed point construction on complete lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file sets up the basic theory of fixed points of a monotone function in a complete lattice.

## Main definitions #

• order_hom.lfp: The least fixed point of a bundled monotone function.
• order_hom.gfp: The greatest fixed point of a bundled monotone function.
• order_hom.prev_fixed: The greatest fixed point of a bundled monotone function smaller than or equal to a given element.
• order_hom.next_fixed: The least fixed point of a bundled monotone function greater than or equal to a given element.
• fixed_points.complete_lattice: The Knaster-Tarski theorem: fixed points of a monotone self-map of a complete lattice form themselves a complete lattice.

## Tags #

fixed point, complete lattice, monotone function

def order_hom.lfp {α : Type u}  :
→o α) →o α

Least fixed point of a monotone function

Equations
def order_hom.gfp {α : Type u}  :
→o α) →o α

Greatest fixed point of a monotone function

Equations
theorem order_hom.lfp_le {α : Type u} (f : α →o α) {a : α} (h : f a a) :
theorem order_hom.lfp_le_fixed {α : Type u} (f : α →o α) {a : α} (h : f a = a) :
theorem order_hom.le_lfp {α : Type u} (f : α →o α) {a : α} (h : (b : α), f b b a b) :
theorem order_hom.map_le_lfp {α : Type u} (f : α →o α) {a : α} (ha : a ) :
f a
@[simp]
theorem order_hom.map_lfp {α : Type u} (f : α →o α) :
f =
theorem order_hom.is_fixed_pt_lfp {α : Type u} (f : α →o α) :
theorem order_hom.lfp_le_map {α : Type u} (f : α →o α) {a : α} (ha : a) :
f a
theorem order_hom.is_least_lfp_le {α : Type u} (f : α →o α) :
is_least {a : α | f a a}
theorem order_hom.is_least_lfp {α : Type u} (f : α →o α) :
theorem order_hom.lfp_induction {α : Type u} (f : α →o α) {p : α Prop} (step : (a : α), p a p (f a)) (hSup : (s : set α), ( (a : α), a s p a) p (has_Sup.Sup s)) :
p
theorem order_hom.le_gfp {α : Type u} (f : α →o α) {a : α} (h : a f a) :
theorem order_hom.gfp_le {α : Type u} (f : α →o α) {a : α} (h : (b : α), b f b b a) :
theorem order_hom.is_fixed_pt_gfp {α : Type u} (f : α →o α) :
@[simp]
theorem order_hom.map_gfp {α : Type u} (f : α →o α) :
f =
theorem order_hom.map_le_gfp {α : Type u} (f : α →o α) {a : α} (ha : a ) :
f a
theorem order_hom.gfp_le_map {α : Type u} (f : α →o α) {a : α} (ha : a) :
f a
theorem order_hom.is_greatest_gfp_le {α : Type u} (f : α →o α) :
is_greatest {a : α | a f a}
theorem order_hom.is_greatest_gfp {α : Type u} (f : α →o α) :
theorem order_hom.gfp_induction {α : Type u} (f : α →o α) {p : α Prop} (step : (a : α), p a p (f a)) (hInf : (s : set α), ( (a : α), a s p a) p (has_Inf.Inf s)) :
p
theorem order_hom.map_lfp_comp {α : Type u} {β : Type v} (f : β →o α) (g : α →o β) :
theorem order_hom.map_gfp_comp {α : Type u} {β : Type v} (f : β →o α) (g : α →o β) :
theorem order_hom.lfp_lfp {α : Type u} (h : α →o α →o α) :
theorem order_hom.gfp_gfp {α : Type u} (h : α →o α →o α) :
theorem order_hom.gfp_const_inf_le {α : Type u} (f : α →o α) (x : α) :
def order_hom.prev_fixed {α : Type u} (f : α →o α) (x : α) (hx : f x x) :

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.prev_fixed x hx is the greatest fixed point of f that is less than or equal to x.

Equations
def order_hom.next_fixed {α : Type u} (f : α →o α) (x : α) (hx : x f x) :

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.next_fixed x hx is the least fixed point of f that is greater than or equal to x.

Equations
theorem order_hom.prev_fixed_le {α : Type u} (f : α →o α) {x : α} (hx : f x x) :
(f.prev_fixed x hx) x
theorem order_hom.le_next_fixed {α : Type u} (f : α →o α) {x : α} (hx : x f x) :
x (f.next_fixed x hx)
theorem order_hom.next_fixed_le {α : Type u} (f : α →o α) {x : α} (hx : x f x) {y : } (h : x y) :
f.next_fixed x hx y
@[simp]
theorem order_hom.next_fixed_le_iff {α : Type u} (f : α →o α) {x : α} (hx : x f x) {y : } :
f.next_fixed x hx y x y
@[simp]
theorem order_hom.le_prev_fixed_iff {α : Type u} (f : α →o α) {x : α} (hx : f x x) {y : } :
y f.prev_fixed x hx y x
theorem order_hom.le_prev_fixed {α : Type u} (f : α →o α) {x : α} (hx : f x x) {y : } (h : y x) :
y f.prev_fixed x hx
theorem order_hom.le_map_sup_fixed_points {α : Type u} (f : α →o α) (x y : ) :
theorem order_hom.map_inf_fixed_points_le {α : Type u} (f : α →o α) (x y : ) :
theorem order_hom.le_map_Sup_subset_fixed_points {α : Type u} (f : α →o α) (A : set α) (hA : A ) :
theorem order_hom.map_Inf_subset_fixed_points_le {α : Type u} (f : α →o α) (A : set α) (hA : A ) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]

Knaster-Tarski Theorem: The fixed points of f form a complete lattice.

Equations