order.complete_boolean_algebra

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 of this typeclass

Instances of other typeclasses for order.frame

order.frame.has_sizeof_inst

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 of this typeclass

Instances of other typeclasses for order.coframe

order.coframe.has_sizeof_inst

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

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 ≤ complete_distrib_lattice.Sup s
Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → complete_distrib_lattice.Sup s ≤ a
Inf : set α → α
Inf_le : ∀ (s : set α) (a : α), a ∈ s → complete_distrib_lattice.Inf s ≤ a
le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ complete_distrib_lattice.Inf s
top : α
bot : α
le_top : ∀ (x : α), x ≤ ⊤
bot_le : ∀ (x : α), ⊥ ≤ x
inf_Sup_le_supr_inf : ∀ (a : α) (s : set α), a ⊓ complete_distrib_lattice.Sup s ≤ ⨆ (b : α) (H : b ∈ s), a ⊓ b
infi_sup_le_sup_Inf : ∀ (a : α) (s : set α), (⨅ (b : α) (H : b ∈ s), a ⊔ b) ≤ a ⊔ complete_distrib_lattice.Inf s

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

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

complete_distrib_lattice.to_coframe = {sup := complete_distrib_lattice.sup _inst_1, le := complete_distrib_lattice.le _inst_1, lt := complete_distrib_lattice.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_distrib_lattice.inf _inst_1, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_distrib_lattice.Sup _inst_1, le_Sup := _, Sup_le := _, Inf := complete_distrib_lattice.Inf _inst_1, Inf_le := _, le_Inf := _, top := complete_distrib_lattice.top _inst_1, bot := complete_distrib_lattice.bot _inst_1, le_top := _, bot_le := _, infi_sup_le_sup_Inf := _}

source

@[protected, instance]

def order_dual.coframe {α : Type u} [order.frame α] :

order.coframe αᵒᵈ

Equations

order_dual.coframe = {sup := complete_lattice.sup (order_dual.complete_lattice α), le := complete_lattice.le (order_dual.complete_lattice α), lt := complete_lattice.lt (order_dual.complete_lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (order_dual.complete_lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (order_dual.complete_lattice α), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (order_dual.complete_lattice α), Inf_le := _, le_Inf := _, top := complete_lattice.top (order_dual.complete_lattice α), bot := complete_lattice.bot (order_dual.complete_lattice α), le_top := _, bot_le := _, infi_sup_le_sup_Inf := _}

source

theorem inf_Sup_eq {α : Type u} [order.frame α] {s : set α} {a : α} :

a ⊓ has_Sup.Sup s = ⨆ (b : α) (H : b ∈ s), a ⊓ b

source

theorem Sup_inf_eq {α : Type u} [order.frame α] {s : set α} {b : α} :

has_Sup.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 α} :

has_Sup.Sup s ⊓ has_Sup.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 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

source

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)

source

theorem Sup_disjoint_iff {α : Type u} [order.frame α] {a : α} {s : set α} :

disjoint (has_Sup.Sup s) a ↔ ∀ (b : α), b ∈ s → disjoint b a

source

theorem disjoint_Sup_iff {α : Type u} [order.frame α] {a : α} {s : set α} :

disjoint a (has_Sup.Sup s) ↔ ∀ (b : α), b ∈ s → disjoint a b

source

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

source

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

source

@[protected, instance]

def pi.frame {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), order.frame (π i)] :

order.frame (Π (i : ι), π i)

Equations

pi.frame = {sup := complete_lattice.sup pi.complete_lattice, le := complete_lattice.le pi.complete_lattice, lt := complete_lattice.lt pi.complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf pi.complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup pi.complete_lattice, le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf pi.complete_lattice, Inf_le := _, le_Inf := _, top := complete_lattice.top pi.complete_lattice, bot := complete_lattice.bot pi.complete_lattice, le_top := _, bot_le := _, inf_Sup_le_supr_inf := _}

source

@[protected, instance]

def frame.to_distrib_lattice {α : Type u} [order.frame α] :

distrib_lattice α

Equations

frame.to_distrib_lattice = distrib_lattice.of_inf_sup_le frame.to_distrib_lattice._proof_1

source

@[protected, instance]

def order_dual.frame {α : Type u} [order.coframe α] :

order.frame αᵒᵈ

Equations

order_dual.frame = {sup := complete_lattice.sup (order_dual.complete_lattice α), le := complete_lattice.le (order_dual.complete_lattice α), lt := complete_lattice.lt (order_dual.complete_lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (order_dual.complete_lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (order_dual.complete_lattice α), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (order_dual.complete_lattice α), Inf_le := _, le_Inf := _, top := complete_lattice.top (order_dual.complete_lattice α), bot := complete_lattice.bot (order_dual.complete_lattice α), le_top := _, bot_le := _, inf_Sup_le_supr_inf := _}

source

theorem sup_Inf_eq {α : Type u} [order.coframe α] {s : set α} {a : α} :

a ⊔ has_Inf.Inf s = ⨅ (b : α) (H : b ∈ s), a ⊔ b

source

theorem Inf_sup_eq {α : Type u} [order.coframe α] {s : set α} {b : α} :

has_Inf.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 α} :

has_Inf.Inf s ⊔ has_Inf.Inf t = ⨅ (p : α × α) (H : p ∈ s ×ˢ t), p.fst ⊔ p.snd

source

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

source

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

source

@[protected, instance]

def pi.coframe {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), order.coframe (π i)] :

order.coframe (Π (i : ι), π i)

Equations

pi.coframe = {sup := complete_lattice.sup pi.complete_lattice, le := complete_lattice.le pi.complete_lattice, lt := complete_lattice.lt pi.complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf pi.complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup pi.complete_lattice, le_Sup := _, Sup_le := _, Inf := has_Inf.Inf pi.has_Inf, Inf_le := _, le_Inf := _, top := complete_lattice.top pi.complete_lattice, bot := complete_lattice.bot pi.complete_lattice, le_top := _, bot_le := _, infi_sup_le_sup_Inf := _}

source

@[protected, instance]

def coframe.to_distrib_lattice {α : Type u} [order.coframe α] :

distrib_lattice α

Equations

coframe.to_distrib_lattice = {sup := order.coframe.sup _inst_1, le := order.coframe.le _inst_1, lt := order.coframe.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := order.coframe.inf _inst_1, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

source

@[protected, instance]

def order_dual.complete_distrib_lattice {α : Type u} [complete_distrib_lattice α] :

complete_distrib_lattice αᵒᵈ

Equations

order_dual.complete_distrib_lattice = {sup := order.frame.sup order_dual.frame, le := order.frame.le order_dual.frame, lt := order.frame.lt order_dual.frame, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := order.frame.inf order_dual.frame, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := order.frame.Sup order_dual.frame, le_Sup := _, Sup_le := _, Inf := order.frame.Inf order_dual.frame, Inf_le := _, le_Inf := _, top := order.frame.top order_dual.frame, bot := order.frame.bot order_dual.frame, le_top := _, bot_le := _, inf_Sup_le_supr_inf := _, infi_sup_le_sup_Inf := _}

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

pi.complete_distrib_lattice = {sup := order.frame.sup pi.frame, le := order.frame.le pi.frame, lt := order.frame.lt pi.frame, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := order.frame.inf pi.frame, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := order.frame.Sup pi.frame, le_Sup := _, Sup_le := _, Inf := order.frame.Inf pi.frame, Inf_le := _, le_Inf := _, top := order.frame.top pi.frame, bot := order.frame.bot pi.frame, le_top := _, bot_le := _, inf_Sup_le_supr_inf := _, infi_sup_le_sup_Inf := _}

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

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
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ᶜ) . "obviously"
himp_eq : (∀ (x y : α), x ⇨ y = y ⊔ xᶜ) . "obviously"
Sup : set α → α
le_Sup : ∀ (s : set α) (a : α), a ∈ s → a ≤ complete_boolean_algebra.Sup s
Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → complete_boolean_algebra.Sup s ≤ a
Inf : set α → α
Inf_le : ∀ (s : set α) (a : α), a ∈ s → complete_boolean_algebra.Inf s ≤ a
le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ complete_boolean_algebra.Inf s
inf_Sup_le_supr_inf : ∀ (a : α) (s : set α), a ⊓ complete_boolean_algebra.Sup s ≤ ⨆ (b : α) (H : b ∈ s), a ⊓ b
infi_sup_le_sup_Inf : ∀ (a : α) (s : set α), (⨅ (b : α) (H : b ∈ s), a ⊔ b) ≤ a ⊔ complete_boolean_algebra.Inf s

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

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

pi.complete_boolean_algebra = {sup := boolean_algebra.sup pi.boolean_algebra, le := boolean_algebra.le pi.boolean_algebra, lt := boolean_algebra.lt pi.boolean_algebra, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := boolean_algebra.inf pi.boolean_algebra, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := boolean_algebra.compl pi.boolean_algebra, sdiff := boolean_algebra.sdiff pi.boolean_algebra, himp := boolean_algebra.himp pi.boolean_algebra, top := boolean_algebra.top pi.boolean_algebra, bot := boolean_algebra.bot pi.boolean_algebra, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _, Sup := complete_distrib_lattice.Sup pi.complete_distrib_lattice, le_Sup := _, Sup_le := _, Inf := complete_distrib_lattice.Inf pi.complete_distrib_lattice, Inf_le := _, le_Inf := _, inf_Sup_le_supr_inf := _, infi_sup_le_sup_Inf := _}

source

@[protected, instance]

def Prop.complete_boolean_algebra :

complete_boolean_algebra Prop

Equations

Prop.complete_boolean_algebra = {sup := boolean_algebra.sup Prop.boolean_algebra, le := boolean_algebra.le Prop.boolean_algebra, lt := boolean_algebra.lt Prop.boolean_algebra, le_refl := Prop.complete_boolean_algebra._proof_1, le_trans := Prop.complete_boolean_algebra._proof_2, lt_iff_le_not_le := Prop.complete_boolean_algebra._proof_3, le_antisymm := Prop.complete_boolean_algebra._proof_4, le_sup_left := Prop.complete_boolean_algebra._proof_5, le_sup_right := Prop.complete_boolean_algebra._proof_6, sup_le := Prop.complete_boolean_algebra._proof_7, inf := boolean_algebra.inf Prop.boolean_algebra, inf_le_left := Prop.complete_boolean_algebra._proof_8, inf_le_right := Prop.complete_boolean_algebra._proof_9, le_inf := Prop.complete_boolean_algebra._proof_10, le_sup_inf := Prop.complete_boolean_algebra._proof_11, compl := boolean_algebra.compl Prop.boolean_algebra, sdiff := boolean_algebra.sdiff Prop.boolean_algebra, himp := boolean_algebra.himp Prop.boolean_algebra, top := boolean_algebra.top Prop.boolean_algebra, bot := boolean_algebra.bot Prop.boolean_algebra, inf_compl_le_bot := Prop.complete_boolean_algebra._proof_12, top_le_sup_compl := Prop.complete_boolean_algebra._proof_13, le_top := Prop.complete_boolean_algebra._proof_14, bot_le := Prop.complete_boolean_algebra._proof_15, sdiff_eq := Prop.complete_boolean_algebra._proof_16, himp_eq := Prop.complete_boolean_algebra._proof_17, Sup := complete_lattice.Sup Prop.complete_lattice, le_Sup := Prop.complete_boolean_algebra._proof_18, Sup_le := Prop.complete_boolean_algebra._proof_19, Inf := complete_lattice.Inf Prop.complete_lattice, Inf_le := Prop.complete_boolean_algebra._proof_20, le_Inf := Prop.complete_boolean_algebra._proof_21, inf_Sup_le_supr_inf := Prop.complete_boolean_algebra._proof_22, infi_sup_le_sup_Inf := Prop.complete_boolean_algebra._proof_23}

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 α} :

(has_Inf.Inf s)ᶜ = ⨆ (i : α) (H : i ∈ s), iᶜ

source

theorem compl_Sup {α : Type u} [complete_boolean_algebra α] {s : set α} :

(has_Sup.Sup s)ᶜ = ⨅ (i : α) (H : i ∈ s), iᶜ

source

theorem compl_Inf' {α : Type u} [complete_boolean_algebra α] {s : set α} :

(has_Inf.Inf s)ᶜ = has_Sup.Sup (has_compl.compl '' s)

source

theorem compl_Sup' {α : Type u} [complete_boolean_algebra α] {s : set α} :

(has_Sup.Sup s)ᶜ = has_Inf.Inf (has_compl.compl '' s)

source

@[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 ⊥ = ⊥) :

order.frame α

Pullback an order.frame along an injection.

Equations

function.injective.frame f hf map_sup map_inf map_Sup map_Inf map_top map_bot = {sup := complete_lattice.sup (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), le := complete_lattice.le (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), lt := complete_lattice.lt (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), Inf_le := _, le_Inf := _, top := complete_lattice.top (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), bot := complete_lattice.bot (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), le_top := _, bot_le := _, inf_Sup_le_supr_inf := _}

source

@[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 ⊥ = ⊥) :

order.coframe α

Pullback an order.coframe along an injection.

Equations

function.injective.coframe f hf map_sup map_inf map_Sup map_Inf map_top map_bot = {sup := complete_lattice.sup (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), le := complete_lattice.le (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), lt := complete_lattice.lt (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), Inf_le := _, le_Inf := _, top := complete_lattice.top (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), bot := complete_lattice.bot (function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot), le_top := _, bot_le := _, infi_sup_le_sup_Inf := _}

source

@[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 ⊥ = ⊥) :

complete_distrib_lattice α

Pullback a complete_distrib_lattice along an injection.

Equations

function.injective.complete_distrib_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot = {sup := order.frame.sup (function.injective.frame f hf map_sup map_inf map_Sup map_Inf map_top map_bot), le := order.frame.le (function.injective.frame f hf map_sup map_inf map_Sup map_Inf map_top map_bot), lt := order.frame.lt (function.injective.frame f hf map_sup map_inf map_Sup map_Inf map_top map_bot), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := order.frame.inf (function.injective.frame f hf map_sup map_inf map_Sup map_Inf map_top map_bot), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := order.frame.Sup (function.injective.frame f hf map_sup map_inf map_Sup map_Inf map_top map_bot), le_Sup := _, Sup_le := _, Inf := order.frame.Inf (function.injective.frame f hf map_sup map_inf map_Sup map_Inf map_top map_bot), Inf_le := _, le_Inf := _, top := order.frame.top (function.injective.frame f hf map_sup map_inf map_Sup map_Inf map_top map_bot), bot := order.frame.bot (function.injective.frame f hf map_sup map_inf map_Sup map_Inf map_top map_bot), le_top := _, bot_le := _, inf_Sup_le_supr_inf := _, infi_sup_le_sup_Inf := _}

source

@[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) :

complete_boolean_algebra α

Pullback a complete_boolean_algebra along an injection.

Equations