mathlib documentation

order.fixed_points

Fixed point construction on complete lattices

def lfp {α : Type u} [complete_lattice α] :
(α → α) → α

Least fixed point of a monotone function

Equations
def gfp {α : Type u} [complete_lattice α] :
(α → α) → α

Greatest fixed point of a monotone function

Equations
theorem lfp_le {α : Type u} [complete_lattice α] {f : α → α} {a : α} :
f a alfp f a

theorem le_lfp {α : Type u} [complete_lattice α] {f : α → α} {a : α} :
(∀ (b : α), f b ba b)a lfp f

theorem lfp_eq {α : Type u} [complete_lattice α] {f : α → α} :
monotone flfp f = f (lfp f)

theorem lfp_induct {α : Type u} [complete_lattice α] {f : α → α} {p : α → Prop} :
monotone f(∀ (a : α), p aa lfp fp (f a))(∀ (s : set α), (∀ (a : α), a sp a)p (Sup s))p (lfp f)

theorem monotone_lfp {α : Type u} [complete_lattice α] :

theorem le_gfp {α : Type u} [complete_lattice α] {f : α → α} {a : α} :
a f aa gfp f

theorem gfp_le {α : Type u} [complete_lattice α] {f : α → α} {a : α} :
(∀ (b : α), b f bb a)gfp f a

theorem gfp_eq {α : Type u} [complete_lattice α] {f : α → α} :
monotone fgfp f = f (gfp f)

theorem gfp_induct {α : Type u} [complete_lattice α] {f : α → α} {p : α → Prop} :
monotone f(∀ (a : α), p agfp f ap (f a))(∀ (s : set α), (∀ (a : α), a sp a)p (Inf s))p (gfp f)

theorem monotone_gfp {α : Type u} [complete_lattice α] :

theorem lfp_comp {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {f : β → α} {g : α → β} :
monotone fmonotone glfp (f g) = f (lfp (g f))

theorem gfp_comp {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {f : β → α} {g : α → β} :
monotone fmonotone ggfp (f g) = f (gfp (g f))

theorem lfp_lfp {α : Type u} [complete_lattice α] {h : α → α → α} :
(∀ ⦃a b c d : α⦄, a bc dh a c h b d)lfp (lfp h) = lfp (λ (x : α), h x x)

theorem gfp_gfp {α : Type u} [complete_lattice α] {h : α → α → α} :
(∀ ⦃a b c d : α⦄, a bc dh a c h b d)gfp (gfp h) = gfp (λ (x : α), h x x)

def fixed_points.prev {α : Type u} [complete_lattice α] :
(α → α)α → α

Equations
def fixed_points.next {α : Type u} [complete_lattice α] :
(α → α)α → α

Equations
theorem fixed_points.prev_le {α : Type u} [complete_lattice α] {f : α → α} {x : α} :

theorem fixed_points.prev_eq {α : Type u} [complete_lattice α] {f : α → α} (hf : monotone f) {a : α} :

def fixed_points.prev_fixed {α : Type u} [complete_lattice α] {f : α → α} (hf : monotone f) (a : α) :

Equations
theorem fixed_points.next_le {α : Type u} [complete_lattice α] {f : α → α} {x : α} :

theorem fixed_points.next_eq {α : Type u} [complete_lattice α] {f : α → α} (hf : monotone f) {a : α} :

def fixed_points.next_fixed {α : Type u} [complete_lattice α] {f : α → α} (hf : monotone f) (a : α) :

Equations
theorem fixed_points.sup_le_f_of_fixed_points {α : Type u} [complete_lattice α] (f : α → α) (hf : monotone f) (x y : (function.fixed_points f)) :
x.val y.val f (x.val y.val)

theorem fixed_points.f_le_inf_of_fixed_points {α : Type u} [complete_lattice α] (f : α → α) (hf : monotone f) (x y : (function.fixed_points f)) :
f (x.val y.val) x.val y.val

theorem fixed_points.Sup_le_f_of_fixed_points {α : Type u} [complete_lattice α] (f : α → α) (hf : monotone f) (A : set α) :

theorem fixed_points.f_le_Inf_of_fixed_points {α : Type u} [complete_lattice α] (f : α → α) (hf : monotone f) (A : set α) :

The fixed points of f form a complete lattice. This cannot be an instance, since it depends on the monotonicity of f.

Equations