class CompleteLattice (L : Type u_1) extends Poset L : Type u_1

• le : L → L → Prop
• le_refl (x : L) : le x x
• le_trans {x y z : L} : le x y → le y z → le x z
• le_antisym {x y : L} : le x y → le y x → x = y
• sup : Set L → L
• inf : Set L → L
• le_sup {s : Set L} {x : L} : x ∈ s → Poset.le x (⊔s)
• sup_le {s : Set L} {y : L} : (∀ (x : L), x ∈ s → Poset.le x y) → Poset.le (⊔s) y
• inf_le {s : Set L} {x : L} : x ∈ s → Poset.le (⊓s) x
• le_inf {s : Set L} {y : L} : (∀ (x : L), x ∈ s → Poset.le y x) → Poset.le y (⊓s)

def «term⊔_» : Lean.ParserDescr

Equations

• «term⊔_» = Lean.ParserDescr.node `«term⊔_» 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊔") (Lean.ParserDescr.cat `term 0))

def «term⊓_» : Lean.ParserDescr

Equations

• «term⊓_» = Lean.ParserDescr.node `«term⊓_» 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊓") (Lean.ParserDescr.cat `term 0))

theorem sup_subset_to_le {L : Type u_1} [CompleteLattice L] {a b : Set L} (subset : a ⊆ b) : Poset.le (⊔a) (⊔b)

theorem sup_pair_eq_right {L : Type u_1} [CompleteLattice L] {x y : L} (h : Poset.le x y) : (⊔{x, y}) = y

theorem inf_pair_eq_left {L : Type u_1} [CompleteLattice L] {x y : L} (h : Poset.le x y) : (⊓{x, y}) = x

def top_of_complete_lattice {L : Type u_1} [CompleteLattice L] : L

Equations

• top_of_complete_lattice = (⊔Set.univ)

def bottom_of_complete_lattice {L : Type u_1} [CompleteLattice L] : L

Equations

• bottom_of_complete_lattice = (⊓Set.univ)

def «term⊤[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «term⊥[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem bottom_is_le_of_complete_lattice {L : Type u_1} [CompleteLattice L] (l : L) : Poset.le bottom_of_complete_lattice l

theorem top_is_ge_of_complete_lattice {L : Type u_1} [CompleteLattice L] (l : L) : Poset.le l top_of_complete_lattice

def lfp {L : Type u_1} [CompleteLattice L] (f : L → L) : L

Equations

• lfp f = (⊓{x : L | Poset.le (f x) x})

axiom Tarskis_fixed_point_theorem_lfp {L : Type u_1} [CompleteLattice L] (f : L → L) (f_mon : monotone f) : f (lfp f) = lfp f

def gfp {L : Type u_1} [CompleteLattice L] (f : L → L) : L

Equations

• gfp f = (⊔{x : L | Poset.le x (f x)})

axiom Tarskis_fixed_point_theorem_gfp {L : Type u_1} [CompleteLattice L] (f : L → L) (f_mon : monotone f) : f (gfp f) = gfp f

theorem prefixed_point_ge_lfp {L : Type u_1} [CompleteLattice L] (f : L → L) (x : L) (h : Poset.le (f x) x) : Poset.le (lfp f) x

theorem postfixed_point_le_gfp {L : Type u_1} [CompleteLattice L] (f : L → L) (x : L) (h : Poset.le x (f x)) : Poset.le x (gfp f)

def dual_complete_lattice {L : Type u_1} [CompleteLattice L] : CompleteLattice L

Equations

• dual_complete_lattice = { toPoset := dual_poset L, sup := fun (s : Set L) => ⊓s, inf := fun (s : Set L) => ⊔s, le_sup := ⋯, sup_le := ⋯, inf_le := ⋯, le_inf := ⋯ }

theorem lfp_eq_gfp_dual {L : Type u_1} [inst : CompleteLattice L] (f : L → L) (_f_mon : monotone f) : lfp f = gfp f

theorem gfp_eq_lfp_dual {L : Type u_1} [inst : CompleteLattice L] (f : L → L) (_f_mon : monotone f) : gfp f = lfp f