# Documentation

Mathlib.Order.CompleteBooleanAlgebra

# 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 ⨅⨅.
• CompleteDistribLattice: Completely distributive lattices: A complete lattice whose ⊓⊓ and ⊔⊔ distribute over ⨆⨆ and ⨅⨅ respectively.
• CompleteBooleanAlgebra: 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 #

class Order.Frame (α : Type u_1) extends :
Type u_1
• In a frame, ⊓⊓ distributes over ⨆⨆.

inf_supₛ_le_supᵢ_inf : ∀ (a : α) (s : Set α), a supₛ s b, h, a b

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

Instances
class Order.Coframe (α : Type u_1) extends :
Type u_1
• In a coframe, ⊔⊔ distributes over ⨅⨅.

infᵢ_sup_le_sup_infₛ : ∀ (a : α) (s : Set α), (b, h, a b) a infₛ s

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

Instances
class CompleteDistribLattice (α : Type u_1) extends :
Type u_1
• In a completely distributive lattice, ⊔⊔ distributes over ⨅⨅.

infᵢ_sup_le_sup_infₛ : ∀ (a : α) (s : Set α), (b, h, a b) a infₛ s

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

Instances
instance CompleteDistribLattice.toCoframe {α : Type u} [inst : ] :
Equations
instance OrderDual.coframe {α : Type u} [inst : ] :
Equations
theorem inf_supₛ_eq {α : Type u} [inst : ] {s : Set α} {a : α} :
a supₛ s = b, h, a b
theorem supₛ_inf_eq {α : Type u} [inst : ] {s : Set α} {b : α} :
supₛ s b = a, h, a b
theorem supᵢ_inf_eq {α : Type u} {ι : Sort w} [inst : ] (f : ια) (a : α) :
(i, f i) a = i, f i a
theorem inf_supᵢ_eq {α : Type u} {ι : Sort w} [inst : ] (a : α) (f : ια) :
(a i, f i) = i, a f i
theorem supᵢ₂_inf_eq {α : Type u} {ι : Sort w} {κ : ιSort u_1} [inst : ] {f : (i : ι) → κ iα} (a : α) :
(i, j, f i j) a = i, j, f i j a
theorem inf_supᵢ₂_eq {α : Type u} {ι : Sort w} {κ : ιSort u_1} [inst : ] {f : (i : ι) → κ iα} (a : α) :
(a i, j, f i j) = i, j, a f i j
theorem supᵢ_inf_supᵢ {α : Type u} [inst : ] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} :
((i, f i) j, g j) = i, f i.fst g i.snd
theorem bsupᵢ_inf_bsupᵢ {α : Type u} [inst : ] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} {s : Set ι} {t : Set ι'} :
((i, h, f i) j, h, g j) = p, h, f p.fst g p.snd
theorem supₛ_inf_supₛ {α : Type u} [inst : ] {s : Set α} {t : Set α} :
supₛ s supₛ t = p, h, p.fst p.snd
theorem supᵢ_disjoint_iff {α : Type u} {ι : Sort w} [inst : ] {a : α} {f : ια} :
Disjoint (i, f i) a ∀ (i : ι), Disjoint (f i) a
theorem disjoint_supᵢ_iff {α : Type u} {ι : Sort w} [inst : ] {a : α} {f : ια} :
Disjoint a (i, f i) ∀ (i : ι), Disjoint a (f i)
theorem supᵢ₂_disjoint_iff {α : Type u} {ι : Sort w} {κ : ιSort u_1} [inst : ] {a : α} {f : (i : ι) → κ iα} :
Disjoint (i, j, f i j) a ∀ (i : ι) (j : κ i), Disjoint (f i j) a
theorem disjoint_supᵢ₂_iff {α : Type u} {ι : Sort w} {κ : ιSort u_1} [inst : ] {a : α} {f : (i : ι) → κ iα} :
Disjoint a (i, j, f i j) ∀ (i : ι) (j : κ i), Disjoint a (f i j)
theorem supₛ_disjoint_iff {α : Type u} [inst : ] {a : α} {s : Set α} :
Disjoint (supₛ s) a ∀ (b : α), b sDisjoint b a
theorem disjoint_supₛ_iff {α : Type u} [inst : ] {a : α} {s : Set α} :
Disjoint a (supₛ s) ∀ (b : α), b sDisjoint a b
theorem supᵢ_inf_of_monotone {α : Type u} [inst : ] {ι : Type u_1} [inst : ] [inst : IsDirected ι fun x x_1 => x x_1] {f : ια} {g : ια} (hf : ) (hg : ) :
(i, f i g i) = (i, f i) i, g i
theorem supᵢ_inf_of_antitone {α : Type u} [inst : ] {ι : Type u_1} [inst : ] [inst : IsDirected ι (Function.swap fun x x_1 => x x_1)] {f : ια} {g : ια} (hf : ) (hg : ) :
(i, f i g i) = (i, f i) i, g i
instance Pi.frame {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → Order.Frame (π i)] :
Order.Frame ((i : ι) → π i)
Equations
• One or more equations did not get rendered due to their size.
instance Frame.toDistribLattice {α : Type u} [inst : ] :
Equations
instance OrderDual.frame {α : Type u} [inst : ] :
Equations
theorem sup_infₛ_eq {α : Type u} [inst : ] {s : Set α} {a : α} :
a infₛ s = b, h, a b
theorem infₛ_sup_eq {α : Type u} [inst : ] {s : Set α} {b : α} :
infₛ s b = a, h, a b
theorem infᵢ_sup_eq {α : Type u} {ι : Sort w} [inst : ] (f : ια) (a : α) :
(i, f i) a = i, f i a
theorem sup_infᵢ_eq {α : Type u} {ι : Sort w} [inst : ] (a : α) (f : ια) :
(a i, f i) = i, a f i
theorem infᵢ₂_sup_eq {α : Type u} {ι : Sort w} {κ : ιSort u_1} [inst : ] {f : (i : ι) → κ iα} (a : α) :
(i, j, f i j) a = i, j, f i j a
theorem sup_infᵢ₂_eq {α : Type u} {ι : Sort w} {κ : ιSort u_1} [inst : ] {f : (i : ι) → κ iα} (a : α) :
(a i, j, f i j) = i, j, a f i j
theorem infᵢ_sup_infᵢ {α : Type u} [inst : ] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} :
((i, f i) i, g i) = i, f i.fst g i.snd
theorem binfᵢ_sup_binfᵢ {α : Type u} [inst : ] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} {s : Set ι} {t : Set ι'} :
((i, h, f i) j, h, g j) = p, h, f p.fst g p.snd
theorem infₛ_sup_infₛ {α : Type u} [inst : ] {s : Set α} {t : Set α} :
infₛ s infₛ t = p, h, p.fst p.snd
theorem infᵢ_sup_of_monotone {α : Type u} [inst : ] {ι : Type u_1} [inst : ] [inst : IsDirected ι (Function.swap fun x x_1 => x x_1)] {f : ια} {g : ια} (hf : ) (hg : ) :
(i, f i g i) = (i, f i) i, g i
theorem infᵢ_sup_of_antitone {α : Type u} [inst : ] {ι : Type u_1} [inst : ] [inst : IsDirected ι fun x x_1 => x x_1] {f : ια} {g : ια} (hf : ) (hg : ) :
(i, f i g i) = (i, f i) i, g i
instance Pi.coframe {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → Order.Coframe (π i)] :
Order.Coframe ((i : ι) → π i)
Equations
• One or more equations did not get rendered due to their size.
instance Coframe.toDistribLattice {α : Type u} [inst : ] :
Equations
instance instCompleteDistribLatticeOrderDual {α : Type u} [inst : ] :
Equations
instance Pi.completeDistribLattice {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → ] :
CompleteDistribLattice ((i : ι) → π i)
Equations
class CompleteBooleanAlgebra (α : Type u_1) extends , , :
Type u_1
• Any upper bound is more than the set supremum.

supₛ_le : ∀ (s : Set α) (a : α), (∀ (b : α), b sb a) → supₛ s a
• toInfSet :
• Any element of a set is more than the set infimum.

infₛ_le : ∀ (s : Set α) (a : α), a sinfₛ s a
• Any lower bound is less than the set infimum.

le_infₛ : ∀ (s : Set α) (a : α), (∀ (b : α), b sa b) → a infₛ s
• In a frame, ⊓⊓ distributes over ⨆⨆.

inf_supₛ_le_supᵢ_inf : ∀ (a : α) (s : Set α), a supₛ s b, h, a b
• In a completely distributive lattice, ⊔⊔ distributes over ⨅⨅.

infᵢ_sup_le_sup_infₛ : ∀ (a : α) (s : Set α), (b, h, a b) a infₛ s

A complete Boolean algebra is a completely distributive Boolean algebra.

Instances
instance Pi.completeBooleanAlgebra {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → ] :
CompleteBooleanAlgebra ((i : ι) → π i)
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
theorem compl_infᵢ {α : Type u} {ι : Sort w} [inst : ] {f : ια} :
infᵢ f = i, f i
theorem compl_supᵢ {α : Type u} {ι : Sort w} [inst : ] {f : ια} :
supᵢ f = i, f i
theorem compl_infₛ {α : Type u} [inst : ] {s : Set α} :
infₛ s = i, h, i
theorem compl_supₛ {α : Type u} [inst : ] {s : Set α} :
supₛ s = i, h, i
theorem compl_infₛ' {α : Type u} [inst : ] {s : Set α} :
infₛ s = supₛ (compl '' s)
theorem compl_supₛ' {α : Type u} [inst : ] {s : Set α} :
supₛ s = infₛ (compl '' s)
def Function.Injective.frame {α : Type u} {β : Type v} [inst : Sup α] [inst : Inf α] [inst : ] [inst : ] [inst : Top α] [inst : Bot α] [inst : ] (f : αβ) (hf : ) (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 (supₛ s) = a, h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = a, h, f a) (map_top : f = ) (map_bot : f = ) :

Pullback an Order.Frame along an injection.

Equations
• One or more equations did not get rendered due to their size.
def Function.Injective.coframe {α : Type u} {β : Type v} [inst : Sup α] [inst : Inf α] [inst : ] [inst : ] [inst : Top α] [inst : Bot α] [inst : ] (f : αβ) (hf : ) (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 (supₛ s) = a, h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = a, h, f a) (map_top : f = ) (map_bot : f = ) :

Pullback an Order.Coframe along an injection.

Equations
• One or more equations did not get rendered due to their size.
def Function.Injective.completeDistribLattice {α : Type u} {β : Type v} [inst : Sup α] [inst : Inf α] [inst : ] [inst : ] [inst : Top α] [inst : Bot α] [inst : ] (f : αβ) (hf : ) (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 (supₛ s) = a, h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = a, h, f a) (map_top : f = ) (map_bot : f = ) :

Pullback a CompleteDistribLattice along an injection.

Equations
• One or more equations did not get rendered due to their size.
def Function.Injective.completeBooleanAlgebra {α : Type u} {β : Type v} [inst : Sup α] [inst : Inf α] [inst : ] [inst : ] [inst : Top α] [inst : Bot α] [inst : ] [inst : ] [inst : ] (f : αβ) (hf : ) (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 (supₛ s) = a, h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = a, h, 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 CompleteBooleanAlgebra along an injection.

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem PUnit.supₛ_eq (s : ) :
@[simp]
theorem PUnit.infₛ_eq (s : ) :