# Frames, completely distributive lattices and complete Boolean algebras #

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

We distinguish two different distributivity properties:

1. inf_iSup_eq : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i (finite distributes over infinite ). This is required by Frame, CompleteDistribLattice, and CompleteBooleanAlgebra (Coframe, etc., require the dual property).
2. iInf_iSup_eq : (⨅ i, ⨆ j, f i j) = ⨆ s, ⨅ i, f i (s i) (infinite distributes over infinite ). This stronger property is called "completely distributive", and is required by CompletelyDistribLattice and CompleteAtomicBooleanAlgebra.

## Typeclasses #

• Order.Frame: Frame: A complete lattice whose distributes over .
• Order.Coframe: Coframe: A complete lattice whose distributes over .
• CompleteDistribLattice: Complete distributive lattices: A complete lattice whose and distribute over and respectively.
• CompleteBooleanAlgebra: Complete Boolean algebra: A Boolean algebra whose and distribute over and respectively.
• CompletelyDistribLattice: Completely distributive lattices: A complete lattice whose and satisfy iInf_iSup_eq.
• CompleteBooleanAlgebra: Complete Boolean algebra: A Boolean algebra whose and distribute over and respectively.
• CompleteAtomicBooleanAlgebra: Complete atomic Boolean algebra: A complete Boolean algebra which is additionally completely distributive. (This implies that it's (co)atom(ist)ic.)

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.

## References #

class Order.Frame (α : Type u_1) extends :
Type u_1

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

• 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
• 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
• sSup : Set αα
• le_sSup : ∀ (s : Set α), as, a sSup s
• sSup_le : ∀ (s : Set α) (a : α), (bs, b a)sSup s a
• sInf : Set αα
• sInf_le : ∀ (s : Set α), as, sInf s a
• le_sInf : ∀ (s : Set α) (a : α), (bs, a b)a sInf s
• top : α
• bot : α
• le_top : ∀ (x : α), x
• bot_le : ∀ (x : α), x
• inf_sSup_le_iSup_inf : ∀ (a : α) (s : Set α), a sSup s bs, a b

distributes over .

Instances
theorem Order.Frame.inf_sSup_le_iSup_inf {α : Type u_1} [self : ] (a : α) (s : Set α) :
a sSup s bs, a b

distributes over .

class Order.Coframe (α : Type u_1) extends :
Type u_1

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

• 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
• 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
• sSup : Set αα
• le_sSup : ∀ (s : Set α), as, a sSup s
• sSup_le : ∀ (s : Set α) (a : α), (bs, b a)sSup s a
• sInf : Set αα
• sInf_le : ∀ (s : Set α), as, sInf s a
• le_sInf : ∀ (s : Set α) (a : α), (bs, a b)a sInf s
• top : α
• bot : α
• le_top : ∀ (x : α), x
• bot_le : ∀ (x : α), x
• iInf_sup_le_sup_sInf : ∀ (a : α) (s : Set α), bs, a b a sInf s

distributes over .

Instances
theorem Order.Coframe.iInf_sup_le_sup_sInf {α : Type u_1} [self : ] (a : α) (s : Set α) :
bs, a b a sInf s

distributes over .

class CompleteDistribLattice (α : Type u_1) extends :
Type u_1

A complete distributive lattice is a complete lattice whose and respectively distribute over and .

• 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
• 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
• sSup : Set αα
• le_sSup : ∀ (s : Set α), as, a sSup s
• sSup_le : ∀ (s : Set α) (a : α), (bs, b a)sSup s a
• sInf : Set αα
• sInf_le : ∀ (s : Set α), as, sInf s a
• le_sInf : ∀ (s : Set α) (a : α), (bs, a b)a sInf s
• top : α
• bot : α
• le_top : ∀ (x : α), x
• bot_le : ∀ (x : α), x
• inf_sSup_le_iSup_inf : ∀ (a : α) (s : Set α), a sSup s bs, a b
• iInf_sup_le_sup_sInf : ∀ (a : α) (s : Set α), bs, a b a sInf s

distributes over .

Instances
theorem CompleteDistribLattice.iInf_sup_le_sup_sInf {α : Type u_1} [self : ] (a : α) (s : Set α) :
bs, a b a sInf s

distributes over .

class CompletelyDistribLattice (α : Type u) extends :

A completely distributive lattice is a complete lattice whose and distribute over each other.

• 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
• 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
• sSup : Set αα
• le_sSup : ∀ (s : Set α), as, a sSup s
• sSup_le : ∀ (s : Set α) (a : α), (bs, b a)sSup s a
• sInf : Set αα
• sInf_le : ∀ (s : Set α), as, sInf s a
• le_sInf : ∀ (s : Set α) (a : α), (bs, a b)a sInf s
• top : α
• bot : α
• le_top : ∀ (x : α), x
• bot_le : ∀ (x : α), x
• iInf_iSup_eq : ∀ {ι : Type u} {κ : ιType u} (f : (a : ι) → κ aα), ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
Instances
theorem CompletelyDistribLattice.iInf_iSup_eq {α : Type u} [self : ] {ι : Type u} {κ : ιType u} (f : (a : ι) → κ aα) :
⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
theorem le_iInf_iSup {α : Type u} {ι : Sort w} {κ : ιSort w'} [] {f : (a : ι) → κ aα} :
⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a) ⨅ (a : ι), ⨆ (b : κ a), f a b
theorem iInf_iSup_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} {f : (a : ι) → κ aα} :
⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
theorem iSup_iInf_le {α : Type u} {ι : Sort w} {κ : ιSort w'} [] {f : (a : ι) → κ aα} :
⨆ (a : ι), ⨅ (b : κ a), f a b ⨅ (g : (a : ι) → κ a), ⨆ (a : ι), f a (g a)
theorem iSup_iInf_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} {f : (a : ι) → κ aα} :
⨆ (a : ι), ⨅ (b : κ a), f a b = ⨅ (g : (a : ι) → κ a), ⨆ (a : ι), f a (g a)
@[instance 100]
Equations
• CompletelyDistribLattice.toCompleteDistribLattice =
@[instance 100]
Equations
• CompleteLinearOrder.toCompletelyDistribLattice =
instance OrderDual.instCoframe {α : Type u} [] :
Equations
• OrderDual.instCoframe = let __spread.0 := OrderDual.instCompleteLattice;
theorem inf_sSup_eq {α : Type u} [] {s : Set α} {a : α} :
a sSup s = bs, a b
theorem sSup_inf_eq {α : Type u} [] {s : Set α} {b : α} :
sSup s b = as, a b
theorem iSup_inf_eq {α : Type u} {ι : Sort w} [] (f : ια) (a : α) :
(⨆ (i : ι), f i) a = ⨆ (i : ι), f i a
theorem inf_iSup_eq {α : Type u} {ι : Sort w} [] (a : α) (f : ια) :
a ⨆ (i : ι), f i = ⨆ (i : ι), a f i
theorem iSup₂_inf_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} [] {f : (i : ι) → κ iα} (a : α) :
(⨆ (i : ι), ⨆ (j : κ i), f i j) a = ⨆ (i : ι), ⨆ (j : κ i), f i j a
theorem inf_iSup₂_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} [] {f : (i : ι) → κ iα} (a : α) :
a ⨆ (i : ι), ⨆ (j : κ i), f i j = ⨆ (i : ι), ⨆ (j : κ i), a f i j
theorem iSup_inf_iSup {α : Type u} [] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} :
(⨆ (i : ι), f i) ⨆ (j : ι'), g j = ⨆ (i : ι × ι'), f i.1 g i.2
theorem biSup_inf_biSup {α : Type u} [] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} {s : Set ι} {t : Set ι'} :
(is, f i) jt, g j = ps ×ˢ t, f p.1 g p.2
theorem sSup_inf_sSup {α : Type u} [] {s : Set α} {t : Set α} :
sSup s sSup t = ps ×ˢ t, p.1 p.2
theorem iSup_disjoint_iff {α : Type u} {ι : Sort w} [] {a : α} {f : ια} :
Disjoint (⨆ (i : ι), f i) a ∀ (i : ι), Disjoint (f i) a
theorem disjoint_iSup_iff {α : Type u} {ι : Sort w} [] {a : α} {f : ια} :
Disjoint a (⨆ (i : ι), f i) ∀ (i : ι), Disjoint a (f i)
theorem iSup₂_disjoint_iff {α : Type u} {ι : Sort w} {κ : ιSort w'} [] {a : α} {f : (i : ι) → κ iα} :
Disjoint (⨆ (i : ι), ⨆ (j : κ i), f i j) a ∀ (i : ι) (j : κ i), Disjoint (f i j) a
theorem disjoint_iSup₂_iff {α : Type u} {ι : Sort w} {κ : ιSort w'} [] {a : α} {f : (i : ι) → κ iα} :
Disjoint a (⨆ (i : ι), ⨆ (j : κ i), f i j) ∀ (i : ι) (j : κ i), Disjoint a (f i j)
theorem sSup_disjoint_iff {α : Type u} [] {a : α} {s : Set α} :
Disjoint (sSup s) a bs, Disjoint b a
theorem disjoint_sSup_iff {α : Type u} [] {a : α} {s : Set α} :
Disjoint a (sSup s) bs, Disjoint a b
theorem iSup_inf_of_monotone {α : Type u} [] {ι : Type u_1} [] [IsDirected ι fun (x x_1 : ι) => x x_1] {f : ια} {g : ια} (hf : ) (hg : ) :
⨆ (i : ι), f i g i = (⨆ (i : ι), f i) ⨆ (i : ι), g i
theorem iSup_inf_of_antitone {α : Type u} [] {ι : Type u_1} [] [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 100]
instance Frame.toDistribLattice {α : Type u} [] :
Equations
• Frame.toDistribLattice =
instance Prod.instFrame {α : Type u} {β : Type v} [] [] :
Order.Frame (α × β)
Equations
• Prod.instFrame = let __spread.0 := Prod.instCompleteLattice;
instance Pi.instFrame {ι : Type u_1} {π : ιType u_2} [(i : ι) → Order.Frame (π i)] :
Order.Frame ((i : ι) → π i)
Equations
• Pi.instFrame = let __spread.0 := Pi.instCompleteLattice;
instance OrderDual.instFrame {α : Type u} [] :
Equations
• OrderDual.instFrame = let __spread.0 := OrderDual.instCompleteLattice;
theorem sup_sInf_eq {α : Type u} [] {s : Set α} {a : α} :
a sInf s = bs, a b
theorem sInf_sup_eq {α : Type u} [] {s : Set α} {b : α} :
sInf s b = as, a b
theorem iInf_sup_eq {α : Type u} {ι : Sort w} [] (f : ια) (a : α) :
(⨅ (i : ι), f i) a = ⨅ (i : ι), f i a
theorem sup_iInf_eq {α : Type u} {ι : Sort w} [] (a : α) (f : ια) :
a ⨅ (i : ι), f i = ⨅ (i : ι), a f i
theorem iInf₂_sup_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} [] {f : (i : ι) → κ iα} (a : α) :
(⨅ (i : ι), ⨅ (j : κ i), f i j) a = ⨅ (i : ι), ⨅ (j : κ i), f i j a
theorem sup_iInf₂_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} [] {f : (i : ι) → κ iα} (a : α) :
a ⨅ (i : ι), ⨅ (j : κ i), f i j = ⨅ (i : ι), ⨅ (j : κ i), a f i j
theorem iInf_sup_iInf {α : Type u} [] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} :
(⨅ (i : ι), f i) ⨅ (i : ι'), g i = ⨅ (i : ι × ι'), f i.1 g i.2
theorem biInf_sup_biInf {α : Type u} [] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} {s : Set ι} {t : Set ι'} :
(is, f i) jt, g j = ps ×ˢ t, f p.1 g p.2
theorem sInf_sup_sInf {α : Type u} [] {s : Set α} {t : Set α} :
sInf s sInf t = ps ×ˢ t, p.1 p.2
theorem iInf_sup_of_monotone {α : Type u} [] {ι : Type u_1} [] [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 iInf_sup_of_antitone {α : Type u} [] {ι : Type u_1} [] [IsDirected ι fun (x x_1 : ι) => x x_1] {f : ια} {g : ια} (hf : ) (hg : ) :
⨅ (i : ι), f i g i = (⨅ (i : ι), f i) ⨅ (i : ι), g i
@[instance 100]
instance Coframe.toDistribLattice {α : Type u} [] :
Equations
• Coframe.toDistribLattice = let __spread.0 := inst;
instance Prod.instCoframe {α : Type u} {β : Type v} [] [] :
Equations
• Prod.instCoframe = let __spread.0 := Prod.instCompleteLattice;
instance Pi.instCoframe {ι : Type u_1} {π : ιType u_2} [(i : ι) → Order.Coframe (π i)] :
Order.Coframe ((i : ι) → π i)
Equations
• Pi.instCoframe = let __spread.0 := Pi.instCompleteLattice;
Equations
• OrderDual.instCompleteDistribLattice = let __spread.0 := OrderDual.instFrame; let __spread.1 := OrderDual.instCoframe;
Equations
• Prod.instCompleteDistribLattice = let __spread.0 := Prod.instFrame; let __spread.1 := Prod.instCoframe;
instance Pi.instCompleteDistribLattice {ι : Type u_1} {π : ιType u_2} [(i : ι) → ] :
CompleteDistribLattice ((i : ι) → π i)
Equations
• Pi.instCompleteDistribLattice = let __spread.0 := Pi.instFrame; let __spread.1 := Pi.instCoframe;
Equations
• OrderDual.instCompletelyDistribLattice = let __spread.0 := OrderDual.instFrame;
instance Prod.instCompletelyDistribLattice {α : Type u} {β : Type v} :
Equations
• Prod.instCompletelyDistribLattice = let __spread.0 := Prod.instFrame;
instance Pi.instCompletelyDistribLattice {ι : Type u_1} {π : ιType u_2} [(i : ι) → ] :
CompletelyDistribLattice ((i : ι) → π i)
Equations
• Pi.instCompletelyDistribLattice = let __spread.0 := Pi.instFrame;
class CompleteBooleanAlgebra (α : Type u_1) extends , , :
Type u_1

A complete Boolean algebra is a Boolean algebra that is also a complete distributive lattice.

It is only completely distributive if it is also atomic.

• 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
• 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
• himp_eq : ∀ (x y : α), x y = y x
• sSup : Set αα
• le_sSup : ∀ (s : Set α), as, a sSup s

Any element of a set is less than the set supremum.

• sSup_le : ∀ (s : Set α) (a : α), (bs, b a)sSup s a

Any upper bound is more than the set supremum.

• sInf : Set αα
• sInf_le : ∀ (s : Set α), as, sInf s a

Any element of a set is more than the set infimum.

• le_sInf : ∀ (s : Set α) (a : α), (bs, a b)a sInf s

Any lower bound is less than the set infimum.

• inf_sSup_le_iSup_inf : ∀ (a : α) (s : Set α), a sSup s bs, a b

distributes over .

• iInf_sup_le_sup_sInf : ∀ (a : α) (s : Set α), bs, a b a sInf s

In a complete distributive lattice, distributes over .

Instances
Equations
• Prod.instCompleteBooleanAlgebra = let __spread.0 := Prod.instBooleanAlgebra; let __spread.1 := Prod.instCompleteDistribLattice;
instance Pi.instCompleteBooleanAlgebra {ι : Type u_1} {π : ιType u_2} [(i : ι) → ] :
CompleteBooleanAlgebra ((i : ι) → π i)
Equations
• Pi.instCompleteBooleanAlgebra = let __spread.0 := Pi.instBooleanAlgebra; let __spread.1 := Pi.instCompleteDistribLattice;
Equations
• OrderDual.instCompleteBooleanAlgebra = let __spread.0 := OrderDual.instBooleanAlgebra; let __spread.1 := OrderDual.instCompleteDistribLattice;
theorem compl_iInf {α : Type u} {ι : Sort w} {f : ια} :
(iInf f) = ⨆ (i : ι), (f i)
theorem compl_iSup {α : Type u} {ι : Sort w} {f : ια} :
(iSup f) = ⨅ (i : ι), (f i)
theorem compl_sInf {α : Type u} {s : Set α} :
(sInf s) = is, i
theorem compl_sSup {α : Type u} {s : Set α} :
(sSup s) = is, i
theorem compl_sInf' {α : Type u} {s : Set α} :
(sInf s) = sSup (compl '' s)
theorem compl_sSup' {α : Type u} {s : Set α} :
(sSup s) = sInf (compl '' s)
theorem iSup_symmDiff_iSup_le {α : Type u} {ι : Sort w} {f : ια} {g : ια} :
symmDiff (⨆ (i : ι), f i) (⨆ (i : ι), g i) ⨆ (i : ι), symmDiff (f i) (g i)

The symmetric difference of two iSups is at most the iSup of the symmetric differences.

theorem biSup_symmDiff_biSup_le {α : Type u} {ι : Sort w} {p : ιProp} {f : (i : ι) → p iα} {g : (i : ι) → p iα} :
symmDiff (⨆ (i : ι), ⨆ (h : p i), f i h) (⨆ (i : ι), ⨆ (h : p i), g i h) ⨆ (i : ι), ⨆ (h : p i), symmDiff (f i h) (g i h)

A biSup version of iSup_symmDiff_iSup_le.

class CompleteAtomicBooleanAlgebra (α : Type u) extends , , , :

A complete atomic Boolean algebra is a complete Boolean algebra that is also completely distributive.

We take iSup_iInf_eq as the definition here, and prove later on that this implies atomicity.

• 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
• 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
• sSup : Set αα
• le_sSup : ∀ (s : Set α), as, a sSup s
• sSup_le : ∀ (s : Set α) (a : α), (bs, b a)sSup s a
• sInf : Set αα
• sInf_le : ∀ (s : Set α), as, sInf s a
• le_sInf : ∀ (s : Set α) (a : α), (bs, a b)a sInf s
• top : α
• bot : α
• le_top : ∀ (x : α), x
• bot_le : ∀ (x : α), x
• iInf_iSup_eq : ∀ {ι : Type u} {κ : ιType u} (f : (a : ι) → κ aα), ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
• le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z

The infimum distributes over the supremum

• compl : αα
• sdiff : ααα
• himp : ααα
• inf_compl_le_bot : ∀ (x : α), x x

The infimum of x and xᶜ is at most

• top_le_sup_compl : ∀ (x : α), x x

The supremum of x and xᶜ is at least

• sdiff_eq : ∀ (x y : α), x \ y = x y

x \ y is equal to x ⊓ yᶜ

• himp_eq : ∀ (x y : α), x y = y x

x ⇨ y is equal to y ⊔ xᶜ

• inf_sSup_le_iSup_inf : ∀ (a : α) (s : Set α), a sSup s bs, a b

distributes over .

• iInf_sup_le_sup_sInf : ∀ (a : α) (s : Set α), bs, a b a sInf s

In a complete distributive lattice, distributes over .

Instances
theorem CompleteAtomicBooleanAlgebra.iInf_sup_le_sup_sInf {α : Type u} [self : ] (a : α) (s : Set α) :
bs, a b a sInf s

In a complete distributive lattice, distributes over .

theorem CompleteAtomicBooleanAlgebra.inf_sSup_le_iSup_inf {α : Type u} [self : ] (a : α) (s : Set α) :
a sSup s bs, a b

distributes over .

instance Prod.instCompleteAtomicBooleanAlgebra {α : Type u} {β : Type v} :
Equations
• Prod.instCompleteAtomicBooleanAlgebra = let __spread.0 := Prod.instBooleanAlgebra; let __spread.1 := Prod.instCompletelyDistribLattice;
instance Pi.instCompleteAtomicBooleanAlgebra {ι : Type u_1} {π : ιType u_2} [(i : ι) → ] :
CompleteAtomicBooleanAlgebra ((i : ι) → π i)
Equations
• Pi.instCompleteAtomicBooleanAlgebra = let __spread.0 := Pi.instCompleteBooleanAlgebra;
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.
@[reducible, inline]
abbrev Function.Injective.frame {α : Type u} {β : Type v} [Sup α] [Inf α] [] [] [Top α] [Bot α] [] (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, 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.
Instances For
@[reducible, inline]
abbrev Function.Injective.coframe {α : Type u} {β : Type v} [Sup α] [Inf α] [] [] [Top α] [Bot α] [] (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, 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.
Instances For
@[reducible, inline]
abbrev Function.Injective.completeDistribLattice {α : Type u} {β : Type v} [Sup α] [Inf α] [] [] [Top α] [Bot α] (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, 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.
Instances For
@[reducible, inline]
abbrev Function.Injective.completelyDistribLattice {α : Type u} {β : Type v} [Sup α] [Inf α] [] [] [Top α] [Bot α] (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, f a) (map_top : f = ) (map_bot : f = ) :

Pullback a CompletelyDistribLattice along an injection.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev Function.Injective.completeBooleanAlgebra {α : Type u} {β : Type v} [Sup α] [Inf α] [] [] [Top α] [Bot α] [] [] (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, 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.
Instances For
@[reducible, inline]
abbrev Function.Injective.completeAtomicBooleanAlgebra {α : Type u} {β : Type v} [Sup α] [Inf α] [] [] [Top α] [Bot α] [] [] (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, 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 CompleteAtomicBooleanAlgebra along an injection.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem PUnit.sSup_eq (s : ) :
@[simp]
theorem PUnit.sInf_eq (s : ) :