mathlib documentation

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 #

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 #

source
@[instance]
def order.frame.to_complete_lattice (α : Type u_2) [self : order.frame α] :
complete_lattice α
source
@[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 ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c
  • Sup : set α → α
  • le_Sup : ∀ (s : set α) (a : α), a ∈ s → a ≤ order.frame.Sup s
  • Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → order.frame.Sup s ≤ a
  • Inf : set α → α
  • Inf_le : ∀ (s : set α) (a : α), a ∈ s → order.frame.Inf s ≤ a
  • le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ order.frame.Inf s
  • top : α
  • bot : α
  • le_top : ∀ (x : α), x ≤ ⊤
  • bot_le : ∀ (x : α), ⊥ ≤ x
  • inf_Sup_le_supr_inf : ∀ (a : α) (s : set α), a ⊓ order.frame.Sup s ≤ ⨆ (b : α) (H : b ∈ s), a ⊓ b

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

Instances
source
@[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 ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c
  • Sup : set α → α
  • le_Sup : ∀ (s : set α) (a : α), a ∈ s → a ≤ order.coframe.Sup s
  • Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → order.coframe.Sup s ≤ a
  • Inf : set α → α
  • Inf_le : ∀ (s : set α) (a : α), a ∈ s → order.coframe.Inf s ≤ a
  • le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ order.coframe.Inf s
  • 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 ⊔ order.coframe.Inf s

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

Instances
source
@[instance]
def order.coframe.to_complete_lattice (α : Type u_2) [self : order.coframe α] :
complete_lattice α
source
@[class]
structure complete_distrib_lattice (α : Type u_2) :
Type u_2

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

Instances
source
@[instance]
def complete_distrib_lattice.to_frame (α : Type u_2) [self : complete_distrib_lattice α] :
order.frame α
source
@[protected, instance]
def complete_distrib_lattice.to_coframe {α : Type u} [complete_distrib_lattice α] :
order.coframe α
Equations
source
@[protected, instance]
def order_dual.coframe {α : Type u} [order.frame α] :
order.coframe (order_dual α)
Equations
source
theorem inf_Sup_eq {α : Type u} [order.frame α] {s : set α} {a : α} :
a ⊓ Sup s = ⨆ (b : α) (H : b ∈ s), a ⊓ b
source
theorem Sup_inf_eq {α : Type u} [order.frame α] {s : set α} {b : α} :
Sup s ⊓ b = ⨆ (a : α) (H : a ∈ s), a ⊓ b
source
theorem supr_inf_eq {α : Type u} {ι : Sort w} [order.frame α] (f : ι → α) (a : α) :
(⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
source
theorem inf_supr_eq {α : Type u} {ι : Sort w} [order.frame α] (a : α) (f : ι → α) :
(a ⊓ ⨆ (i : ι), f i) = ⨆ (i : ι), a ⊓ f i
source
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
source
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
source
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
source
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
source
theorem Sup_inf_Sup {α : Type u} [order.frame α] {s t : set α} :
Sup s ⊓ Sup t = ⨆ (p : α × α) (H : p ∈ s ×ˢ t), p.fst ⊓ p.snd
source
theorem supr_disjoint_iff {α : Type u} {ι : Sort w} [order.frame α] {a : α} {f : ι → α} :
disjoint (⨆ (i : ι), f i) a ↔ ∀ (i : ι), disjoint (f i) a
source
theorem disjoint_supr_iff {α : Type u} {ι : Sort w} [order.frame α] {a : α} {f : ι → α} :
disjoint a (⨆ (i : ι), f i) ↔ ∀ (i : ι), disjoint a (f i)
source
theorem Sup_disjoint_iff {α : Type u} [order.frame α] {a : α} {s : set α} :
disjoint (Sup s) a ↔ ∀ (b : α), b ∈ s → disjoint b a
source
theorem disjoint_Sup_iff {α : Type u} [order.frame α] {a : α} {s : set α} :
disjoint a (Sup s) ↔ ∀ (b : α), b ∈ s → disjoint a b
source
@[protected, instance]
def pi.frame {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), order.frame (π i)] :
order.frame (Π (i : ι), π i)
Equations
source
@[protected, instance]
def order_dual.frame {α : Type u} [order.coframe α] :
order.frame (order_dual α)
Equations
source
theorem sup_Inf_eq {α : Type u} [order.coframe α] {s : set α} {a : α} :
a ⊔ Inf s = ⨅ (b : α) (H : b ∈ s), a ⊔ b
source
theorem Inf_sup_eq {α : Type u} [order.coframe α] {s : set α} {b : α} :
Inf s ⊔ b = ⨅ (a : α) (H : a ∈ s), a ⊔ b
source
theorem infi_sup_eq {α : Type u} {ι : Sort w} [order.coframe α] (f : ι → α) (a : α) :
(⨅ (i : ι), f i) ⊔ a = ⨅ (i : ι), f i ⊔ a
source
theorem sup_infi_eq {α : Type u} {ι : Sort w} [order.coframe α] (a : α) (f : ι → α) :
(a ⊔ ⨅ (i : ι), f i) = ⨅ (i : ι), a ⊔ f i
source
theorem binfi_sup_eq {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} [order.coframe α] {f : Π (i : ι), κ i → α} (a : α) :
(⨅ (i : ι) (j : κ i), f i j) ⊔ a = ⨅ (i : ι) (j : κ i), f i j ⊔ a
source
theorem sup_binfi_eq {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} [order.coframe α] {f : Π (i : ι), κ i → α} (a : α) :
(a ⊔ ⨅ (i : ι) (j : κ i), f i j) = ⨅ (i : ι) (j : κ i), a ⊔ f i j
source
theorem infi_sup_infi {α : Type u} [order.coframe α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} :
((⨅ (i : ι), f i) ⊔ ⨅ (i : ι'), g i) = ⨅ (i : ι × ι'), f i.fst ⊔ g i.snd
source
theorem binfi_sup_binfi {α : Type u} [order.coframe α] {ι : 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
source
theorem Inf_sup_Inf {α : Type u} [order.coframe α] {s t : set α} :
Inf s ⊔ Inf t = ⨅ (p : α × α) (H : p ∈ s ×ˢ t), p.fst ⊔ p.snd
source
@[protected, instance]
def pi.coframe {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), order.coframe (π i)] :
order.coframe (Π (i : ι), π i)
Equations
source
@[protected, instance]
def order_dual.complete_distrib_lattice {α : Type u} [complete_distrib_lattice α] :
complete_distrib_lattice (order_dual α)
Equations
source
@[protected, instance]
def pi.complete_distrib_lattice {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), complete_distrib_lattice (π i)] :
complete_distrib_lattice (Π (i : ι), π i)
Equations
source
@[protected, instance]
def complete_distrib_lattice.to_distrib_lattice {α : Type u} [d : complete_distrib_lattice α] :
distrib_lattice α
Equations
source
@[instance]
def complete_boolean_algebra.to_complete_distrib_lattice (α : Type u_2) [self : complete_boolean_algebra α] :
complete_distrib_lattice α
source
@[class]
structure complete_boolean_algebra (α : Type u_2) :
Type u_2

A complete Boolean algebra is a completely distributive Boolean algebra.

Instances
source
@[instance]
def complete_boolean_algebra.to_boolean_algebra (α : Type u_2) [self : complete_boolean_algebra α] :
boolean_algebra α
source
@[protected, instance]
def pi.complete_boolean_algebra {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), complete_boolean_algebra (π i)] :
complete_boolean_algebra (Π (i : ι), π i)
Equations
source
@[protected, instance]
def Prop.complete_boolean_algebra  :
complete_boolean_algebra Prop
Equations
source
theorem compl_infi {α : Type u} {ι : Sort w} [complete_boolean_algebra α] {f : ι → α} :
(infi f)ᶜ = ⨆ (i : ι), (f i)ᶜ
source
theorem compl_supr {α : Type u} {ι : Sort w} [complete_boolean_algebra α] {f : ι → α} :
(supr f)ᶜ = ⨅ (i : ι), (f i)ᶜ
source
theorem compl_Inf {α : Type u} [complete_boolean_algebra α] {s : set α} :
(Inf s)ᶜ = ⨆ (i : α) (H : i ∈ s), iᶜ
source
theorem compl_Sup {α : Type u} [complete_boolean_algebra α] {s : set α} :
(Sup s)ᶜ = ⨅ (i : α) (H : i ∈ s), iᶜ
source
theorem compl_Inf' {α : Type u} [complete_boolean_algebra α] {s : set α} :
(Inf s)ᶜ = Sup (compl '' s)
source
theorem compl_Sup' {α : Type u} [complete_boolean_algebra α] {s : set α} :
(Sup s)ᶜ = Inf (compl '' s)
source
@[protected]
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 (Sup s) = ⨆ (a : α) (H : a ∈ s), f a) (map_Inf : ∀ (s : set α), f (Inf s) = ⨅ (a : α) (H : a ∈ s), f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) :
order.frame α

Pullback an order.frame along an injection.

Equations
source
@[protected]
def function.injective.coframe {α : Type u} {β : Type v} [has_sup α] [has_inf α] [has_Sup α] [has_Inf α] [has_top α] [has_bot α] [order.coframe β] (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 (Sup s) = ⨆ (a : α) (H : a ∈ s), f a) (map_Inf : ∀ (s : set α), f (Inf s) = ⨅ (a : α) (H : a ∈ s), f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) :
order.coframe α

Pullback an order.coframe along an injection.

Equations
source
@[protected]
def function.injective.complete_distrib_lattice {α : Type u} {β : Type v} [has_sup α] [has_inf α] [has_Sup α] [has_Inf α] [has_top α] [has_bot α] [complete_distrib_lattice β] (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 (Sup s) = ⨆ (a : α) (H : a ∈ s), f a) (map_Inf : ∀ (s : set α), f (Inf s) = ⨅ (a : α) (H : a ∈ s), f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) :
complete_distrib_lattice α

Pullback a complete_distrib_lattice along an injection.

Equations
source
@[protected]
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 α] [complete_boolean_algebra β] (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 (Sup s) = ⨆ (a : α) (H : a ∈ s), f a) (map_Inf : ∀ (s : set α), f (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) :
complete_boolean_algebra α

Pullback a complete_boolean_algebra along an injection.

Equations