mathlib documentation

order.fixed_points

Fixed point construction on complete lattices

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

Least fixed point of a monotone function

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

Greatest fixed point of a monotone function

Equations
source
theorem lfp_le {α : Type u} [complete_lattice α] {f : α → α} {a : α} (h : f a ≤ a) :
lfp f ≤ a

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

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

source
theorem lfp_induct {α : Type u} [complete_lattice α] {f : α → α} {p : α → Prop} (m : monotone f) (step : ∀ (a : α), p a → a ≤ lfp f → p (f a)) (sup : ∀ (s : set α), (∀ (a : α), a ∈ s → p a) → p (Sup s)) :
p (lfp f)

source
theorem monotone_lfp {α : Type u} [complete_lattice α] :
monotone lfp

source
theorem le_gfp {α : Type u} [complete_lattice α] {f : α → α} {a : α} (h : a ≤ f a) :
a ≤ gfp f

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

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

source
theorem gfp_induct {α : Type u} [complete_lattice α] {f : α → α} {p : α → Prop} (m : monotone f) (step : ∀ (a : α), p a → gfp f ≤ a → p (f a)) (inf : ∀ (s : set α), (∀ (a : α), a ∈ s → p a) → p (Inf s)) :
p (gfp f)

source
theorem monotone_gfp {α : Type u} [complete_lattice α] :
monotone gfp

source
theorem lfp_comp {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {f : β → α} {g : α → β} (m_f : monotone f) (m_g : monotone g) :
lfp (f ∘ g) = f (lfp (g ∘ f))

source
theorem gfp_comp {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {f : β → α} {g : α → β} (m_f : monotone f) (m_g : monotone g) :
gfp (f ∘ g) = f (gfp (g ∘ f))

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

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

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

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

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

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

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

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

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

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

Equations
source
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)

source
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

source
theorem fixed_points.Sup_le_f_of_fixed_points {α : Type u} [complete_lattice α] (f : α → α) (hf : monotone f) (A : set α) (HA : A ⊆ function.fixed_points f) :
Sup A ≤ f (Sup A)

source
theorem fixed_points.f_le_Inf_of_fixed_points {α : Type u} [complete_lattice α] (f : α → α) (hf : monotone f) (A : set α) (HA : A ⊆ function.fixed_points f) :
f (Inf A) ≤ Inf A

source
def fixed_points.complete_lattice {α : Type u} [complete_lattice α] (f : α → α) (hf : monotone f) :
complete_lattice ↥(function.fixed_points f)

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

Equations