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 #

@[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 sa order.frame.Sup s
  • Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b sb a)order.frame.Sup s a
  • Inf : set α → α
  • Inf_le : ∀ (s : set α) (a : α), a sorder.frame.Inf s a
  • le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b sa 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 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 sa order.coframe.Sup s
  • Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b sb a)order.coframe.Sup s a
  • Inf : set α → α
  • Inf_le : ∀ (s : set α) (a : α), a sorder.coframe.Inf s a
  • le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b sa 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 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

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]
theorem inf_Sup_eq {α : Type u} [order.frame α] {s : set α} {a : α} :
a has_Sup.Sup s = ⨆ (b : α) (H : b s), a b
theorem Sup_inf_eq {α : Type u} [order.frame α] {s : set α} {b : α} :
has_Sup.Sup s 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 α} :
has_Sup.Sup s has_Sup.Sup t = ⨆ (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 : ι → α} :
disjoint a (⨆ (i : ι), f i) ∀ (i : ι), disjoint a (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 → α} :
disjoint a (⨆ (i : ι) (j : κ i), f i j) ∀ (i : ι) (j : κ i), disjoint a (f i j)
theorem Sup_disjoint_iff {α : Type u} [order.frame α] {a : α} {s : set α} :
disjoint (has_Sup.Sup s) a ∀ (b : α), b sdisjoint b a
theorem disjoint_Sup_iff {α : Type u} [order.frame α] {a : α} {s : set α} :
disjoint a (has_Sup.Sup s) ∀ (b : α), b sdisjoint a b
theorem supr_inf_of_monotone {α : Type u} [order.frame α] {ι : Type u_1} [preorder ι] [is_directed ι has_le.le] {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 ι] [is_directed ι (function.swap has_le.le)] {f g : ι → α} (hf : antitone f) (hg : antitone g) :
(⨆ (i : ι), f i g i) = (⨆ (i : ι), f i) ⨆ (i : ι), g i
@[protected, instance]
Equations
theorem sup_Inf_eq {α : Type u} [order.coframe α] {s : set α} {a : α} :
a has_Inf.Inf s = ⨅ (b : α) (H : b s), a b
theorem Inf_sup_eq {α : Type u} [order.coframe α] {s : set α} {b : α} :
has_Inf.Inf s b = ⨅ (a : α) (H : a s), a b
theorem infi_sup_eq {α : Type u} {ι : Sort w} [order.coframe α] (f : ι → α) (a : α) :
(⨅ (i : ι), f i) a = ⨅ (i : ι), f i a
theorem sup_infi_eq {α : Type u} {ι : Sort w} [order.coframe α] (a : α) (f : ι → α) :
(a ⨅ (i : ι), f i) = ⨅ (i : ι), a f i
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
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
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
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
theorem Inf_sup_Inf {α : Type u} [order.coframe α] {s t : set α} :
has_Inf.Inf s has_Inf.Inf t = ⨅ (p : α × α) (H : p s ×ˢ t), p.fst p.snd
theorem infi_sup_of_monotone {α : Type u} [order.coframe α] {ι : Type u_1} [preorder ι] [is_directed ι (function.swap has_le.le)] {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} [order.coframe α] {ι : Type u_1} [preorder ι] [is_directed ι has_le.le] {f g : ι → α} (hf : antitone f) (hg : antitone g) :
(⨅ (i : ι), f i g i) = (⨅ (i : ι), f i) ⨅ (i : ι), g i
@[protected, instance]
Equations
@[class]
structure complete_boolean_algebra (α : Type u_2) :
Type u_2

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
@[protected, instance]
Equations
theorem compl_infi {α : Type u} {ι : Sort w} [complete_boolean_algebra α] {f : ι → α} :
(infi f) = ⨆ (i : ι), (f i)
theorem compl_supr {α : Type u} {ι : Sort w} [complete_boolean_algebra α] {f : ι → α} :
(supr f) = ⨅ (i : ι), (f i)
theorem compl_Inf {α : Type u} [complete_boolean_algebra α] {s : set α} :
(has_Inf.Inf s) = ⨆ (i : α) (H : i s), i
theorem compl_Sup {α : Type u} [complete_boolean_algebra α] {s : set α} :
(has_Sup.Sup s) = ⨅ (i : α) (H : i s), i
@[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 α] [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 (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 α] [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 (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 α] [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 (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) :
has_Sup.Sup s = punit.star
@[simp]
theorem punit.Inf_eq (s : set punit) :
has_Inf.Inf s = punit.star