mathlib3 documentation

order.complete_boolean_algebra

Frames, completely distributive lattices and Boolean algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
@[class]
structure order.frame (α : Type u_2) :
Type u_2

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

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]
@[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
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 s disjoint b a
theorem disjoint_Sup_iff {α : Type u} [order.frame α] {a : α} {s : set α} :
disjoint a (has_Sup.Sup s) (b : α), b s disjoint 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