# mathlibdocumentation

order.complete_boolean_algebra

# Frames, completely distributive lattices and Boolean algebras #

In this file we define and provide API for frames, completely distributive lattices and completely distributive Boolean algebras.

## Typeclasses #

• order.frame: Frame: A complete lattice whose ⊓ distributes over ⨆.
• order.coframe: Coframe: A complete lattice whose ⊔ distributes over ⨅.
• complete_distrib_lattice: Completely distributive lattices: A complete lattice whose ⊓ and ⊔ distribute over ⨆ and ⨅ respectively.
• complete_boolean_algebra: Completely distributive Boolean algebra: A Boolean algebra whose ⊓ and ⊔ distribute over ⨆ and ⨅ respectively.

A set of opens gives rise to a topological space precisely if it forms a frame. Such a frame is also completely distributive, but not all frames are. filter is a coframe but not a completely distributive lattice.

## TODO #

Add instances for prod

## References #

@[instance]
def order.frame.to_complete_lattice (α : Type u_2) [self : order.frame α] :
@[class]
structure order.frame (α : Type u_2) :
Type u_2
• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca b c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a b a
• inf_le_right : ∀ (a b : α), a b b
• le_inf : ∀ (a b c : α), a ba ca b c
• Sup : set α → α
• le_Sup : ∀ (s : set α) (a : α), a s
• Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b sb a)
• Inf : set α → α
• Inf_le : ∀ (s : set α) (a : α), a s
• le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b sa b)
• top : α
• bot : α
• le_top : ∀ (x : α), x
• bot_le : ∀ (x : α), x
• inf_Sup_le_supr_inf : ∀ (a : α) (s : set α), ⨆ (b : α) (H : b s), a b

A frame, aka complete Heyting algebra, is a complete lattice whose ⊓ distributes over ⨆.

Instances of this typeclass
Instances of other typeclasses for order.frame
• order.frame.has_sizeof_inst
@[class]
structure order.coframe (α : Type u_2) :
Type u_2
• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca b c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a b a
• inf_le_right : ∀ (a b : α), a b b
• le_inf : ∀ (a b c : α), a ba ca b c
• Sup : set α → α
• le_Sup : ∀ (s : set α) (a : α), a s
• Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b sb a)
• Inf : set α → α
• Inf_le : ∀ (s : set α) (a : α), a s
• le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b sa b)
• top : α
• bot : α
• le_top : ∀ (x : α), x
• bot_le : ∀ (x : α), x
• infi_sup_le_sup_Inf : ∀ (a : α) (s : set α), (⨅ (b : α) (H : b s), a b)

A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice whose ⊔ distributes over ⨅.

Instances of this typeclass
Instances of other typeclasses for order.coframe
• order.coframe.has_sizeof_inst
@[instance]
def order.coframe.to_complete_lattice (α : Type u_2) [self : order.coframe α] :
@[class]
structure complete_distrib_lattice (α : Type u_2) :
Type u_2
• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca b c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a b a
• inf_le_right : ∀ (a b : α), a b b
• le_inf : ∀ (a b c : α), a ba ca b c
• Sup : set α → α
• le_Sup : ∀ (s : set α) (a : α), a s
• Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b sb a)
• Inf : set α → α
• Inf_le : ∀ (s : set α) (a : α), a s
• le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b sa b)
• top : α
• bot : α
• le_top : ∀ (x : α), x
• bot_le : ∀ (x : α), x
• inf_Sup_le_supr_inf : ∀ (a : α) (s : set α), ⨆ (b : α) (H : b s), a b
• infi_sup_le_sup_Inf : ∀ (a : α) (s : set α), (⨅ (b : α) (H : b s), a b)

A completely distributive lattice is a complete lattice whose ⊔ and ⊓ respectively distribute over ⨅ and ⨆.

Instances of this typeclass
Instances of other typeclasses for complete_distrib_lattice
• complete_distrib_lattice.has_sizeof_inst
@[instance]
def complete_distrib_lattice.to_frame (α : Type u_2) [self : complete_distrib_lattice α] :
@[protected, instance]
def order_dual.coframe {α : Type u} [order.frame α] :
Equations
theorem inf_Sup_eq {α : Type u} [order.frame α] {s : set α} {a : α} :
a = ⨆ (b : α) (H : b s), a b
theorem Sup_inf_eq {α : Type u} [order.frame α] {s : set α} {b : α} :
b = ⨆ (a : α) (H : a s), a b
theorem supr_inf_eq {α : Type u} {ι : Sort w} [order.frame α] (f : ι → α) (a : α) :
(⨆ (i : ι), f i) a = ⨆ (i : ι), f i a
theorem inf_supr_eq {α : Type u} {ι : Sort w} [order.frame α] (a : α) (f : ι → α) :
(a ⨆ (i : ι), f i) = ⨆ (i : ι), a f i
theorem bsupr_inf_eq {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} [order.frame α] {f : Π (i : ι), κ i → α} (a : α) :
(⨆ (i : ι) (j : κ i), f i j) a = ⨆ (i : ι) (j : κ i), f i j a
theorem inf_bsupr_eq {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} [order.frame α] {f : Π (i : ι), κ i → α} (a : α) :
(a ⨆ (i : ι) (j : κ i), f i j) = ⨆ (i : ι) (j : κ i), a f i j
theorem supr_inf_supr {α : Type u} [order.frame α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} :
((⨆ (i : ι), f i) ⨆ (j : ι'), g j) = ⨆ (i : ι × ι'), f i.fst g i.snd
theorem bsupr_inf_bsupr {α : Type u} [order.frame α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} {s : set ι} {t : set ι'} :
((⨆ (i : ι) (H : i s), f i) ⨆ (j : ι') (H : j t), g j) = ⨆ (p : ι × ι') (H : p s ×ˢ t), f p.fst g p.snd
theorem Sup_inf_Sup {α : Type u} [order.frame α] {s t : set α} :
= ⨆ (p : α × α) (H : p s ×ˢ t), p.fst p.snd
theorem supr_disjoint_iff {α : Type u} {ι : Sort w} [order.frame α] {a : α} {f : ι → α} :
disjoint (⨆ (i : ι), f i) a ∀ (i : ι), disjoint (f i) a
theorem disjoint_supr_iff {α : Type u} {ι : Sort w} [order.frame α] {a : α} {f : ι → α} :
(⨆ (i : ι), f i) ∀ (i : ι), (f i)
theorem supr₂_disjoint_iff {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} [order.frame α] {a : α} {f : Π (i : ι), κ i → α} :
disjoint (⨆ (i : ι) (j : κ i), f i j) a ∀ (i : ι) (j : κ i), disjoint (f i j) a
theorem disjoint_supr₂_iff {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} [order.frame α] {a : α} {f : Π (i : ι), κ i → α} :
(⨆ (i : ι) (j : κ i), f i j) ∀ (i : ι) (j : κ i), (f i j)
theorem Sup_disjoint_iff {α : Type u} [order.frame α] {a : α} {s : set α} :
a ∀ (b : α), b s a
theorem disjoint_Sup_iff {α : Type u} [order.frame α] {a : α} {s : set α} :
(has_Sup.Sup s) ∀ (b : α), b s b
theorem supr_inf_of_monotone {α : Type u} [order.frame α] {ι : Type u_1} [preorder ι] {f g : ι → α} (hf : monotone f) (hg : monotone g) :
(⨆ (i : ι), f i g i) = (⨆ (i : ι), f i) ⨆ (i : ι), g i
theorem supr_inf_of_antitone {α : Type u} [order.frame α] {ι : Type u_1} [preorder ι] {f g : ι → α} (hf : antitone f) (hg : antitone g) :
(⨆ (i : ι), f i g i) = (⨆ (i : ι), f i) ⨆ (i : ι), g i
@[protected, instance]
def pi.frame {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), order.frame (π i)] :
order.frame (Π (i : ι), π i)
Equations
@[protected, instance]
def frame.to_distrib_lattice {α : Type u} [order.frame α] :
Equations
@[protected, instance]
def order_dual.frame {α : Type u}  :
Equations
theorem sup_Inf_eq {α : Type u} {s : set α} {a : α} :
a = ⨅ (b : α) (H : b s), a b
theorem Inf_sup_eq {α : Type u} {s : set α} {b : α} :
b = ⨅ (a : α) (H : a s), a b
theorem infi_sup_eq {α : Type u} {ι : Sort w} (f : ι → α) (a : α) :
(⨅ (i : ι), f i) a = ⨅ (i : ι), f i a
theorem sup_infi_eq {α : Type u} {ι : Sort w} (a : α) (f : ι → α) :
(a ⨅ (i : ι), f i) = ⨅ (i : ι), a f i
theorem binfi_sup_eq {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} {f : Π (i : ι), κ i → α} (a : α) :
(⨅ (i : ι) (j : κ i), f i j) a = ⨅ (i : ι) (j : κ i), f i j a
theorem sup_binfi_eq {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} {f : Π (i : ι), κ i → α} (a : α) :
(a ⨅ (i : ι) (j : κ i), f i j) = ⨅ (i : ι) (j : κ i), a f i j
theorem infi_sup_infi {α : Type u} {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} :
((⨅ (i : ι), f i) ⨅ (i : ι'), g i) = ⨅ (i : ι × ι'), f i.fst g i.snd
theorem binfi_sup_binfi {α : Type u} {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} {s : set ι} {t : set ι'} :
((⨅ (i : ι) (H : i s), f i) ⨅ (j : ι') (H : j t), g j) = ⨅ (p : ι × ι') (H : p s ×ˢ t), f p.fst g p.snd
theorem Inf_sup_Inf {α : Type u} {s t : set α} :
= ⨅ (p : α × α) (H : p s ×ˢ t), p.fst p.snd
theorem infi_sup_of_monotone {α : Type u} {ι : Type u_1} [preorder ι] {f g : ι → α} (hf : monotone f) (hg : monotone g) :
(⨅ (i : ι), f i g i) = (⨅ (i : ι), f i) ⨅ (i : ι), g i
theorem infi_sup_of_antitone {α : Type u} {ι : Type u_1} [preorder ι] {f g : ι → α} (hf : antitone f) (hg : antitone g) :
(⨅ (i : ι), f i g i) = (⨅ (i : ι), f i) ⨅ (i : ι), g i
@[protected, instance]
def pi.coframe {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), order.coframe (π i)] :
order.coframe (Π (i : ι), π i)
Equations
@[protected, instance]
def coframe.to_distrib_lattice {α : Type u}  :
Equations
@[protected, instance]
def order_dual.complete_distrib_lattice {α : Type u}  :
Equations
@[protected, instance]
def pi.complete_distrib_lattice {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), ] :
complete_distrib_lattice (Π (i : ι), π i)
Equations
@[class]
structure complete_boolean_algebra (α : Type u_2) :
Type u_2
• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca b c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a b a
• inf_le_right : ∀ (a b : α), a b b
• le_inf : ∀ (a b c : α), a ba ca b c
• le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z
• compl : α → α
• sdiff : α → α → α
• himp : α → α → α
• top : α
• bot : α
• inf_compl_le_bot : ∀ (x : α), x x
• top_le_sup_compl : ∀ (x : α), x x
• le_top : ∀ (a : α), a
• bot_le : ∀ (a : α), a
• sdiff_eq : (∀ (x y : α), x \ y = x y) . "obviously"
• himp_eq : (∀ (x y : α), x y = y x) . "obviously"
• Sup : set α → α
• le_Sup : ∀ (s : set α) (a : α), a s
• Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b sb a)
• Inf : set α → α
• Inf_le : ∀ (s : set α) (a : α), a s
• le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b sa b)
• inf_Sup_le_supr_inf : ∀ (a : α) (s : set α), ⨆ (b : α) (H : b s), a b
• infi_sup_le_sup_Inf : ∀ (a : α) (s : set α), (⨅ (b : α) (H : b s), a b)

A complete Boolean algebra is a completely distributive Boolean algebra.

Instances of this typeclass
Instances of other typeclasses for complete_boolean_algebra
• complete_boolean_algebra.has_sizeof_inst
@[instance]
@[protected, instance]
def pi.complete_boolean_algebra {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), ] :
complete_boolean_algebra (Π (i : ι), π i)
Equations
@[protected, instance]
Equations
theorem compl_infi {α : Type u} {ι : Sort w} {f : ι → α} :
(infi f) = ⨆ (i : ι), (f i)
theorem compl_supr {α : Type u} {ι : Sort w} {f : ι → α} :
(supr f) = ⨅ (i : ι), (f i)
theorem compl_Inf {α : Type u} {s : set α} :
(has_Inf.Inf s) = ⨆ (i : α) (H : i s), i
theorem compl_Sup {α : Type u} {s : set α} :
(has_Sup.Sup s) = ⨅ (i : α) (H : i s), i
theorem compl_Inf' {α : Type u} {s : set α} :
theorem compl_Sup' {α : Type u} {s : set α} :
@[protected, reducible]
def function.injective.frame {α : Type u} {β : Type v} [has_sup α] [has_inf α] [has_Sup α] [has_Inf α] [has_top α] [has_bot α] [order.frame β] (f : α → β) (hf : function.injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) (map_Sup : ∀ (s : set α), f (has_Sup.Sup s) = ⨆ (a : α) (H : a s), f a) (map_Inf : ∀ (s : set α), f (has_Inf.Inf s) = ⨅ (a : α) (H : a s), f a) (map_top : f = ) (map_bot : f = ) :

Pullback an order.frame along an injection.

Equations
@[protected, reducible]
def function.injective.coframe {α : Type u} {β : Type v} [has_sup α] [has_inf α] [has_Sup α] [has_Inf α] [has_top α] [has_bot α] (f : α → β) (hf : function.injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) (map_Sup : ∀ (s : set α), f (has_Sup.Sup s) = ⨆ (a : α) (H : a s), f a) (map_Inf : ∀ (s : set α), f (has_Inf.Inf s) = ⨅ (a : α) (H : a s), f a) (map_top : f = ) (map_bot : f = ) :

Pullback an order.coframe along an injection.

Equations
@[protected, reducible]
def function.injective.complete_distrib_lattice {α : Type u} {β : Type v} [has_sup α] [has_inf α] [has_Sup α] [has_Inf α] [has_top α] [has_bot α] (f : α → β) (hf : function.injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) (map_Sup : ∀ (s : set α), f (has_Sup.Sup s) = ⨆ (a : α) (H : a s), f a) (map_Inf : ∀ (s : set α), f (has_Inf.Inf s) = ⨅ (a : α) (H : a s), f a) (map_top : f = ) (map_bot : f = ) :

Pullback a complete_distrib_lattice along an injection.

Equations
@[protected, reducible]
def function.injective.complete_boolean_algebra {α : Type u} {β : Type v} [has_sup α] [has_inf α] [has_Sup α] [has_Inf α] [has_top α] [has_bot α] [has_compl α] [has_sdiff α] (f : α → β) (hf : function.injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) (map_Sup : ∀ (s : set α), f (has_Sup.Sup s) = ⨆ (a : α) (H : a s), f a) (map_Inf : ∀ (s : set α), f (has_Inf.Inf s) = ⨅ (a : α) (H : a s), f a) (map_top : f = ) (map_bot : f = ) (map_compl : ∀ (a : α), f a = (f a)) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

Pullback a complete_boolean_algebra along an injection.

Equations
@[protected, instance]
Equations
@[simp]
theorem punit.Sup_eq (s : set punit) :
= punit.star
@[simp]
theorem punit.Inf_eq (s : set punit) :
= punit.star