Completely distributive lattices and Boolean algebras #
In this file there are definitions and an API for completely distributive lattices and completely distributive Boolean algebras.
Typeclasses #
complete_distrib_lattice: Completely distributive lattices: A complete lattice whose⊓and⊔distribute over⨆and⨅respectively.complete_boolean_algebra: Completely distributive Boolean algebra: A Boolean algebra whose⊓and⊔distribute over⨆and⨅respectively.
@[instance]
def
complete_distrib_lattice.to_complete_lattice
(α : Type u_1)
[self : complete_distrib_lattice α] :
@[class]
- 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
- infi_sup_le_sup_Inf : ∀ (a : α) (s : set α), (⨅ (b : α) (H : b ∈ s), a ⊔ b) ≤ a ⊔ complete_distrib_lattice.Inf s
- inf_Sup_le_supr_inf : ∀ (a : α) (s : set α), a ⊓ complete_distrib_lattice.Sup s ≤ ⨆ (b : α) (H : b ∈ s), a ⊓ b
A complete distributive lattice is a bit stronger than the name might suggest; perhaps completely distributive lattice is more descriptive, as this class includes a requirement that the lattice join distribute over arbitrary infima, and similarly for the dual.
@[protected, instance]
Equations
- order_dual.complete_distrib_lattice = {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 := _, inf_Sup_le_supr_inf := _}
theorem
bsupr_inf_eq
{α : Type u}
[complete_distrib_lattice α]
{p : α → Prop}
{f : Π (i : α), p i → α}
(a : α) :
theorem
inf_bsupr_eq
{α : Type u}
[complete_distrib_lattice α]
(a : α)
{p : α → Prop}
{f : Π (i : α), p i → α} :
theorem
binfi_sup_eq
{α : Type u}
[complete_distrib_lattice α]
{p : α → Prop}
{f : Π (i : α), p i → α}
(a : α) :
theorem
sup_binfi_eq
{α : Type u}
[complete_distrib_lattice α]
(a : α)
{p : α → Prop}
{f : Π (i : α), p i → α} :
@[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 := 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 := _, infi_sup_le_sup_Inf := _, inf_Sup_le_supr_inf := _}
theorem
supr_disjoint_iff
{α : Type u}
{ι : Sort w}
[complete_distrib_lattice α]
{a : α}
{f : ι → α} :
theorem
disjoint_supr_iff
{α : Type u}
{ι : Sort w}
[complete_distrib_lattice α]
{a : α}
{f : ι → α} :
@[protected, instance]
Equations
- complete_distrib_lattice.to_distrib_lattice = {sup := complete_distrib_lattice.sup d, le := complete_distrib_lattice.le d, lt := complete_distrib_lattice.lt d, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_distrib_lattice.inf d, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}
@[instance]
def
complete_boolean_algebra.to_complete_distrib_lattice
(α : Type u_1)
[self : complete_boolean_algebra α] :
@[class]
- 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
- sdiff : α → α → α
- bot : α
- sup_inf_sdiff : ∀ (a b : α), a ⊓ b ⊔ a \ b = a
- inf_inf_sdiff : ∀ (a b : α), a ⊓ b ⊓ a \ b = ⊥
- compl : α → α
- top : α
- 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ᶜ
- 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
- infi_sup_le_sup_Inf : ∀ (a : α) (s : set α), (⨅ (b : α) (H : 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
A complete Boolean algebra is a completely distributive Boolean algebra.
@[instance]
def
complete_boolean_algebra.to_boolean_algebra
(α : Type u_1)
[self : complete_boolean_algebra α] :
@[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 := _, sdiff := boolean_algebra.sdiff pi.boolean_algebra, bot := boolean_algebra.bot pi.boolean_algebra, sup_inf_sdiff := _, inf_inf_sdiff := _, compl := boolean_algebra.compl pi.boolean_algebra, top := boolean_algebra.top pi.boolean_algebra, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_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 := _, infi_sup_le_sup_Inf := _, inf_Sup_le_supr_inf := _}
@[protected, instance]
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, sdiff := boolean_algebra.sdiff Prop.boolean_algebra, bot := boolean_algebra.bot Prop.boolean_algebra, sup_inf_sdiff := Prop.complete_boolean_algebra._proof_12, inf_inf_sdiff := Prop.complete_boolean_algebra._proof_13, compl := boolean_algebra.compl Prop.boolean_algebra, top := boolean_algebra.top Prop.boolean_algebra, inf_compl_le_bot := Prop.complete_boolean_algebra._proof_14, top_le_sup_compl := Prop.complete_boolean_algebra._proof_15, le_top := Prop.complete_boolean_algebra._proof_16, bot_le := Prop.complete_boolean_algebra._proof_17, sdiff_eq := Prop.complete_boolean_algebra._proof_18, Sup := complete_lattice.Sup Prop.complete_lattice, le_Sup := Prop.complete_boolean_algebra._proof_19, Sup_le := Prop.complete_boolean_algebra._proof_20, Inf := complete_lattice.Inf Prop.complete_lattice, Inf_le := Prop.complete_boolean_algebra._proof_21, le_Inf := Prop.complete_boolean_algebra._proof_22, infi_sup_le_sup_Inf := Prop.complete_boolean_algebra._proof_23, inf_Sup_le_supr_inf := Prop.complete_boolean_algebra._proof_24}