mathlib docs: order.fixed

source

def lfp {α : Type u} [complete_lattice α] :

(α → α) → α

Least fixed point of a monotone function

Equations

lfp f = has_Inf.Inf {a : α | f a ≤ a}

source

def gfp {α : Type u} [complete_lattice α] :

(α → α) → α

Greatest fixed point of a monotone function

Equations

gfp f = has_Sup.Sup {a : α | a ≤ f a}

source

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

f a ≤ a → lfp f ≤ a

source

theorem le_lfp {α : Type u} [complete_lattice α] {f : α → α} {a : α} :

(∀ (b : α), f b ≤ b → a ≤ b) → a ≤ lfp f

source

theorem lfp_eq {α : Type u} [complete_lattice α] {f : α → α} :

monotone f → lfp f = f (lfp f)

source

theorem lfp_induct {α : Type u} [complete_lattice α] {f : α → α} {p : α → Prop} :

monotone f → (∀ (a : α), p a → a ≤ lfp f → p (f a)) → (∀ (s : set α), (∀ (a : α), a ∈ s → p a) → p (has_Sup.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 : α} :

a ≤ f a → a ≤ gfp f

source

theorem gfp_le {α : Type u} [complete_lattice α] {f : α → α} {a : α} :

(∀ (b : α), b ≤ f b → b ≤ a) → gfp f ≤ a

source

theorem gfp_eq {α : Type u} [complete_lattice α] {f : α → α} :

monotone f → gfp f = f (gfp f)

source

theorem gfp_induct {α : Type u} [complete_lattice α] {f : α → α} {p : α → Prop} :

monotone f → (∀ (a : α), p a → gfp f ≤ a → p (f a)) → (∀ (s : set α), (∀ (a : α), a ∈ s → p a) → p (has_Inf.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 : α → β} :

monotone f → monotone g → lfp (f ∘ g) = f (lfp (g ∘ f))

source

theorem gfp_comp {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {f : β → α} {g : α → β} :

monotone f → monotone g → gfp (f ∘ g) = f (gfp (g ∘ f))

source

theorem lfp_lfp {α : Type u} [complete_lattice α] {h : α → α → α} :

(∀ ⦃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 : α → α → α} :

(∀ ⦃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 α] :

(α → α) → α → α

Equations

fixed_points.prev f x = gfp (λ (z : α), x ⊓ f z)

source

def fixed_points.next {α : Type u} [complete_lattice α] :

(α → α) → α → α

Equations

fixed_points.next f x = lfp (λ (z : α), x ⊔ f z)

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 : α} :

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 : α) :

f a ≤ a → ↥(function.fixed_points f)

Equations

fixed_points.prev_fixed hf a h = ⟨fixed_points.prev f a, _⟩

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 : α} :

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 : α) :

a ≤ f a → ↥(function.fixed_points f)

Equations

fixed_points.next_fixed hf a h = ⟨fixed_points.next f a, _⟩

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 α) :

A ⊆ function.fixed_points f → has_Sup.Sup A ≤ f (has_Sup.Sup A)

source

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

A ⊆ function.fixed_points f → f (has_Inf.Inf A) ≤ has_Inf.Inf A

source

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

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

fixed_points.complete_lattice f hf = {sup := λ (x y : ↥(function.fixed_points f)), fixed_points.next_fixed hf (x.val ⊔ y.val) _, le := λ (x y : ↥(function.fixed_points f)), x.val ≤ y.val, lt := bounded_lattice.lt._default (λ (x y : ↥(function.fixed_points f)), x.val ≤ y.val), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (x y : ↥(function.fixed_points f)), fixed_points.prev_fixed hf (x.val ⊓ y.val) _, inf_le_left := _, inf_le_right := _, le_inf := _, top := fixed_points.prev_fixed hf ⊤ _, le_top := _, bot := fixed_points.next_fixed hf ⊥ _, bot_le := _, Sup := λ (A : set ↥(function.fixed_points f)), fixed_points.next_fixed hf (has_Sup.Sup (subtype.val '' A)) _, Inf := λ (A : set ↥(function.fixed_points f)), fixed_points.prev_fixed hf (has_Inf.Inf (subtype.val '' A)) _, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}

mathlib documentation

order.fixed_points

Fixed point construction on complete lattices

General documentation

Additional documentation

Library

mathlib documentation

order.​fixed_points

Fixed point construction on complete lattices

General documentation

Additional documentation

Library

order.fixed_points