Theory of complete lattices
Main definitions
SupandInfare the supremum and the infimum of a set;supr (f : ι → α)andinfi (f : ι → α)are indexed supremum and infimum of a function, defined asSupandInfof the range of this function;class complete_lattice: a bounded lattice such thatSup sis always the least upper boundary ofsandInf sis always the greatest lower boundary ofs;class complete_linear_order: a linear ordered complete lattice.
Naming conventions
We use Sup/Inf/supr/infi for the corresponding functions in the statement. Sometimes we
also use bsupr/binfi for "boundedsupremum or infimum, i.e. one of⨆ i ∈ s, f i,
⨆ i (hi : p i), f i, or more generally⨆ i (hi : p i), f i hi`.
Notation
@[class]
- Inf : set α → α
class for the Inf operator
Instances
- complete_lattice.to_has_Inf
- conditionally_complete_lattice.to_has_Inf
- order_dual.has_Inf
- pi.has_Inf
- prod.has_Inf
- submonoid.has_Inf
- add_submonoid.has_Inf
- subgroup.has_Inf
- add_subgroup.has_Inf
- submodule.has_Inf
- setoid.has_Inf
- con.has_Inf
- add_con.has_Inf
- subsemiring.has_Inf
- with_top.has_Inf
- with_bot.has_Inf
- nat.has_Inf
- real.has_Inf
- nnreal.has_Inf
- uniform_space.has_Inf
- convex_cone.has_Inf
- ereal.has_Inf
- measure_theory.measure.has_Inf
@[instance]
Equations
- order_dual.has_Sup α = {Sup := has_Inf.Inf _inst_1}
@[instance]
Equations
- order_dual.has_Inf α = {Inf := has_Sup.Sup _inst_1}
@[instance]
@[class]
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- 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_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
- inf : α → α → α
- inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
- inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
- le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
- top : α
- le_top : ∀ (a : α), a ≤ ⊤
- bot : α
- bot_le : ∀ (a : α), ⊥ ≤ a
- Sup : set α → α
- Inf : set α → α
- le_Sup : ∀ (s : set α) (a : α), a ∈ s → a ≤ complete_lattice.Sup s
- Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → complete_lattice.Sup s ≤ a
- Inf_le : ∀ (s : set α) (a : α), a ∈ s → complete_lattice.Inf s ≤ a
- le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ complete_lattice.Inf s
A complete lattice is a bounded lattice which has suprema and infima for every subset.
Instances
- complete_linear_order.to_complete_lattice
- complete_distrib_lattice.to_complete_lattice
- order_dual.complete_lattice
- complete_lattice_Prop
- pi.complete_lattice
- prod.complete_lattice
- set.lattice_set
- submonoid.complete_lattice
- add_submonoid.complete_lattice
- subgroup.complete_lattice
- add_subgroup.complete_lattice
- submodule.complete_lattice
- setoid.complete_lattice
- con.complete_lattice
- add_con.complete_lattice
- subsemiring.complete_lattice
- algebra.complete_lattice
- rel.complete_lattice
- with_top.with_bot.complete_lattice
- filter.complete_lattice
- topological_space.complete_lattice
- topological_space.opens.complete_lattice
- affine_subspace.complete_lattice
- uniform_space.complete_lattice
- convex_cone.complete_lattice
- ereal.complete_lattice
- setoid.partition.complete_lattice
- measurable_space.complete_lattice
- measure_theory.outer_measure.complete_lattice
- measure_theory.measure.complete_lattice
@[instance]
@[instance]
def
complete_lattice_of_Inf
(α : Type u_1)
[H1 : partial_order α]
[H2 : has_Inf α] :
(∀ (s : set α), is_glb s (has_Inf.Inf s)) → complete_lattice α
Create a complete_lattice from a partial_order and Inf function
that returns the greatest lower bound of a set. Usually this constructor provides
poor definitional equalities, so it should be used with
.. complete_lattice_of_Inf α _.
Equations
- complete_lattice_of_Inf α is_glb_Inf = {sup := λ (a b : α), has_Inf.Inf {x : α | a ≤ x ∧ b ≤ x}, le := partial_order.le H1, lt := partial_order.lt H1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (a b : α), has_Inf.Inf {a, b}, inf_le_left := _, inf_le_right := _, le_inf := _, top := has_Inf.Inf ∅, le_top := _, bot := has_Inf.Inf set.univ, bot_le := _, Sup := λ (s : set α), has_Inf.Inf (upper_bounds s), Inf := has_Inf.Inf H2, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
def
complete_lattice_of_Sup
(α : Type u_1)
[H1 : partial_order α]
[H2 : has_Sup α] :
(∀ (s : set α), is_lub s (has_Sup.Sup s)) → complete_lattice α
Create a complete_lattice from a partial_order and Sup function
that returns the least upper bound of a set. Usually this constructor provides
poor definitional equalities, so it should be used with
.. complete_lattice_of_Sup α _.
Equations
- complete_lattice_of_Sup α is_lub_Sup = {sup := λ (a b : α), has_Sup.Sup {a, b}, le := partial_order.le H1, lt := partial_order.lt H1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (a b : α), has_Sup.Sup {x : α | x ≤ a ∧ x ≤ b}, inf_le_left := _, inf_le_right := _, le_inf := _, top := has_Sup.Sup set.univ, le_top := _, bot := has_Sup.Sup ∅, bot_le := _, Sup := has_Sup.Sup H2, Inf := λ (s : set α), has_Sup.Sup (lower_bounds s), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
@[instance]
@[class]
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- 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_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
- inf : α → α → α
- inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
- inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
- le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
- top : α
- le_top : ∀ (a : α), a ≤ ⊤
- bot : α
- bot_le : ∀ (a : α), ⊥ ≤ a
- Sup : set α → α
- Inf : set α → α
- le_Sup : ∀ (s : set α) (a : α), a ∈ s → a ≤ complete_linear_order.Sup s
- Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → complete_linear_order.Sup s ≤ a
- Inf_le : ∀ (s : set α) (a : α), a ∈ s → complete_linear_order.Inf s ≤ a
- le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ complete_linear_order.Inf s
- le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
- decidable_le : decidable_rel has_le.le
- decidable_eq : decidable_eq α
- decidable_lt : decidable_rel has_lt.lt
A complete linear order is a linear order whose lattice structure is complete.
@[instance]
@[instance]
Equations
- order_dual.complete_lattice α = {sup := bounded_lattice.sup (order_dual.bounded_lattice α), le := bounded_lattice.le (order_dual.bounded_lattice α), lt := bounded_lattice.lt (order_dual.bounded_lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf (order_dual.bounded_lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, top := bounded_lattice.top (order_dual.bounded_lattice α), le_top := _, bot := bounded_lattice.bot (order_dual.bounded_lattice α), bot_le := _, Sup := has_Sup.Sup (order_dual.has_Sup α), Inf := has_Inf.Inf (order_dual.has_Inf α), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
@[instance]
Equations
- order_dual.complete_linear_order α = {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 := _, top := complete_lattice.top (order_dual.complete_lattice α), le_top := _, bot := complete_lattice.bot (order_dual.complete_lattice α), bot_le := _, Sup := complete_lattice.Sup (order_dual.complete_lattice α), Inf := complete_lattice.Inf (order_dual.complete_lattice α), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _, le_total := _, decidable_le := decidable_linear_order.decidable_le (order_dual.decidable_linear_order α), decidable_eq := decidable_linear_order.decidable_eq (order_dual.decidable_linear_order α), decidable_lt := decidable_linear_order.decidable_lt (order_dual.decidable_linear_order α)}
theorem
Sup_le
{α : Type u_1}
[complete_lattice α]
{s : set α}
{a : α} :
(∀ (b : α), b ∈ s → b ≤ a) → has_Sup.Sup s ≤ a
theorem
le_Inf
{α : Type u_1}
[complete_lattice α]
{s : set α}
{a : α} :
(∀ (b : α), b ∈ s → a ≤ b) → a ≤ has_Inf.Inf s
theorem
is_lub.Sup_eq
{α : Type u_1}
[complete_lattice α]
{s : set α}
{a : α} :
is_lub s a → has_Sup.Sup s = a
theorem
is_glb.Inf_eq
{α : Type u_1}
[complete_lattice α]
{s : set α}
{a : α} :
is_glb s a → has_Inf.Inf s = a
theorem
le_Sup_of_le
{α : Type u_1}
[complete_lattice α]
{s : set α}
{a b : α} :
b ∈ s → a ≤ b → a ≤ has_Sup.Sup s
theorem
Inf_le_of_le
{α : Type u_1}
[complete_lattice α]
{s : set α}
{a b : α} :
b ∈ s → b ≤ a → has_Inf.Inf s ≤ a
theorem
Sup_le_Sup
{α : Type u_1}
[complete_lattice α]
{s t : set α} :
s ⊆ t → has_Sup.Sup s ≤ has_Sup.Sup t
theorem
Inf_le_Inf
{α : Type u_1}
[complete_lattice α]
{s t : set α} :
s ⊆ t → has_Inf.Inf t ≤ has_Inf.Inf s
@[simp]
theorem
Sup_le_iff
{α : Type u_1}
[complete_lattice α]
{s : set α}
{a : α} :
has_Sup.Sup s ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a
@[simp]
theorem
le_Inf_iff
{α : Type u_1}
[complete_lattice α]
{s : set α}
{a : α} :
a ≤ has_Inf.Inf s ↔ ∀ (b : α), b ∈ s → a ≤ b
theorem
Inf_le_Sup
{α : Type u_1}
[complete_lattice α]
{s : set α} :
s.nonempty → has_Inf.Inf s ≤ has_Sup.Sup s
theorem
Sup_union
{α : Type u_1}
[complete_lattice α]
{s t : set α} :
has_Sup.Sup (s ∪ t) = has_Sup.Sup s ⊔ has_Sup.Sup t
theorem
Sup_inter_le
{α : Type u_1}
[complete_lattice α]
{s t : set α} :
has_Sup.Sup (s ∩ t) ≤ has_Sup.Sup s ⊓ has_Sup.Sup t
theorem
Inf_union
{α : Type u_1}
[complete_lattice α]
{s t : set α} :
has_Inf.Inf (s ∪ t) = has_Inf.Inf s ⊓ has_Inf.Inf t
theorem
le_Inf_inter
{α : Type u_1}
[complete_lattice α]
{s t : set α} :
has_Inf.Inf s ⊔ has_Inf.Inf t ≤ has_Inf.Inf (s ∩ t)
@[simp]
theorem
Sup_insert
{α : Type u_1}
[complete_lattice α]
{a : α}
{s : set α} :
has_Sup.Sup (has_insert.insert a s) = a ⊔ has_Sup.Sup s
@[simp]
theorem
Inf_insert
{α : Type u_1}
[complete_lattice α]
{a : α}
{s : set α} :
has_Inf.Inf (has_insert.insert a s) = a ⊓ has_Inf.Inf s
theorem
Sup_le_Sup_of_subset_instert_bot
{α : Type u_1}
[complete_lattice α]
{s t : set α} :
s ⊆ has_insert.insert ⊥ t → has_Sup.Sup s ≤ has_Sup.Sup t
theorem
Inf_le_Inf_of_subset_insert_top
{α : Type u_1}
[complete_lattice α]
{s t : set α} :
s ⊆ has_insert.insert ⊤ t → has_Inf.Inf t ≤ has_Inf.Inf s
@[simp]
@[simp]
theorem
Inf_lt_iff
{α : Type u_1}
[complete_linear_order α]
{s : set α}
{b : α} :
has_Inf.Inf s < b ↔ ∃ (a : α) (H : a ∈ s), a < b
theorem
lt_Sup_iff
{α : Type u_1}
[complete_linear_order α]
{s : set α}
{b : α} :
b < has_Sup.Sup s ↔ ∃ (a : α) (H : a ∈ s), b < a
theorem
le_supr_of_le
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{s : ι → α}
{a : α}
(i : ι) :
theorem
le_bsupr
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{p : ι → Prop}
{f : Π (i : ι), p i → α}
(i : ι)
(hi : p i) :
f i hi ≤ ⨆ (i : ι) (hi : p i), f i hi
theorem
bsupr_le
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{a : α}
{p : ι → Prop}
{f : Π (i : ι), p i → α} :
theorem
bsupr_le_supr
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
(p : ι → Prop)
(f : ι → α) :
(⨆ (i : ι) (H : p i), f i) ≤ ⨆ (i : ι), f i
theorem
supr_le_supr2
{α : Type u_1}
{ι : Sort u_4}
{ι₂ : Sort u_5}
[complete_lattice α]
{s : ι → α}
{t : ι₂ → α} :
theorem
bsupr_le_bsupr
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{p : ι → Prop}
{f g : Π (i : ι), p i → α} :
theorem
supr_le_supr_const
{α : Type u_1}
{ι : Sort u_4}
{ι₂ : Sort u_5}
[complete_lattice α]
{a : α} :
(ι → ι₂) → ((⨆ (i : ι), a) ≤ ⨆ (j : ι₂), a)
@[simp]
theorem
Sup_eq_supr
{α : Type u_1}
[complete_lattice α]
{s : set α} :
has_Sup.Sup s = ⨆ (a : α) (H : a ∈ s), a
theorem
monotone.le_map_supr
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[complete_lattice α]
{s : ι → α}
[complete_lattice β]
{f : α → β} :
theorem
monotone.le_map_supr2
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[complete_lattice α]
[complete_lattice β]
{f : α → β}
(hf : monotone f)
{ι' : ι → Sort u_3}
(s : Π (i : ι), ι' i → α) :
(⨆ (i : ι) (h : ι' i), f (s i h)) ≤ f (⨆ (i : ι) (h : ι' i), s i h)
theorem
monotone.le_map_Sup
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
[complete_lattice β]
{s : set α}
{f : α → β} :
monotone f → (⨆ (a : α) (H : a ∈ s), f a) ≤ f (has_Sup.Sup s)
theorem
supr_comp_le
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{ι' : Sort u_2}
(f : ι' → α)
(g : ι → ι') :
(⨆ (x : ι), f (g x)) ≤ ⨆ (y : ι'), f y
theorem
monotone.supr_comp_eq
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[complete_lattice α]
[preorder β]
{f : β → α}
(hf : monotone f)
{s : ι → β} :
theorem
function.surjective.supr_comp
{ι : Sort u_4}
{ι₂ : Sort u_5}
{α : Type u_1}
[has_Sup α]
{f : ι → ι₂}
(hf : function.surjective f)
(g : ι₂ → α) :
(⨆ (x : ι), g (f x)) = ⨆ (y : ι₂), g y
theorem
supr_congr
{ι : Sort u_4}
{ι₂ : Sort u_5}
{α : Type u_1}
[has_Sup α]
{f : ι → α}
{g : ι₂ → α}
(h : ι → ι₂) :
function.surjective h → (∀ (x : ι), g (h x) = f x) → ((⨆ (x : ι), f x) = ⨆ (y : ι₂), g y)
theorem
infi_le_of_le
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{s : ι → α}
{a : α}
(i : ι) :
theorem
binfi_le
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{p : ι → Prop}
{f : Π (i : ι), p i → α}
(i : ι)
(hi : p i) :
(⨅ (i : ι) (hi : p i), f i hi) ≤ f i hi
theorem
le_binfi
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{a : α}
{p : ι → Prop}
{f : Π (i : ι), p i → α} :
theorem
infi_le_binfi
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
(p : ι → Prop)
(f : ι → α) :
(⨅ (i : ι), f i) ≤ ⨅ (i : ι) (H : p i), f i
theorem
infi_le_infi2
{α : Type u_1}
{ι : Sort u_4}
{ι₂ : Sort u_5}
[complete_lattice α]
{s : ι → α}
{t : ι₂ → α} :
theorem
binfi_le_binfi
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{p : ι → Prop}
{f g : Π (i : ι), p i → α} :
theorem
infi_le_infi_const
{α : Type u_1}
{ι : Sort u_4}
{ι₂ : Sort u_5}
[complete_lattice α]
{a : α} :
(ι₂ → ι) → ((⨅ (i : ι), a) ≤ ⨅ (j : ι₂), a)
@[simp]
theorem
Inf_eq_infi
{α : Type u_1}
[complete_lattice α]
{s : set α} :
has_Inf.Inf s = ⨅ (a : α) (H : a ∈ s), a
theorem
monotone.map_infi_le
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[complete_lattice α]
{s : ι → α}
[complete_lattice β]
{f : α → β} :
theorem
monotone.map_infi2_le
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[complete_lattice α]
[complete_lattice β]
{f : α → β}
(hf : monotone f)
{ι' : ι → Sort u_3}
(s : Π (i : ι), ι' i → α) :
f (⨅ (i : ι) (h : ι' i), s i h) ≤ ⨅ (i : ι) (h : ι' i), f (s i h)
theorem
monotone.map_Inf_le
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
[complete_lattice β]
{s : set α}
{f : α → β} :
monotone f → (f (has_Inf.Inf s) ≤ ⨅ (a : α) (H : a ∈ s), f a)
theorem
le_infi_comp
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{ι' : Sort u_2}
(f : ι' → α)
(g : ι → ι') :
(⨅ (y : ι'), f y) ≤ ⨅ (x : ι), f (g x)
theorem
monotone.infi_comp_eq
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[complete_lattice α]
[preorder β]
{f : β → α}
(hf : monotone f)
{s : ι → β} :
theorem
function.surjective.infi_comp
{ι : Sort u_4}
{ι₂ : Sort u_5}
{α : Type u_1}
[has_Inf α]
{f : ι → ι₂}
(hf : function.surjective f)
(g : ι₂ → α) :
(⨅ (x : ι), g (f x)) = ⨅ (y : ι₂), g y
theorem
infi_congr
{ι : Sort u_4}
{ι₂ : Sort u_5}
{α : Type u_1}
[has_Inf α]
{f : ι → α}
{g : ι₂ → α}
(h : ι → ι₂) :
function.surjective h → (∀ (x : ι), g (h x) = f x) → ((⨅ (x : ι), f x) = ⨅ (y : ι₂), g y)
theorem
infi_const
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
[nonempty ι]
{a : α} :
(⨅ (b : ι), a) = a
theorem
supr_const
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
[nonempty ι]
{a : α} :
(⨆ (b : ι), a) = a
@[simp]
@[simp]
@[simp]
theorem
infi_pos
{α : Type u_1}
[complete_lattice α]
{p : Prop}
{f : p → α}
(hp : p) :
(⨅ (h : p), f h) = f hp
@[simp]
theorem
supr_pos
{α : Type u_1}
[complete_lattice α]
{p : Prop}
{f : p → α}
(hp : p) :
(⨆ (h : p), f h) = f hp
theorem
infi_comm
{α : Type u_1}
{ι : Sort u_4}
{ι₂ : Sort u_5}
[complete_lattice α]
{f : ι → ι₂ → α} :
(⨅ (i : ι) (j : ι₂), f i j) = ⨅ (j : ι₂) (i : ι), f i j
theorem
supr_comm
{α : Type u_1}
{ι : Sort u_4}
{ι₂ : Sort u_5}
[complete_lattice α]
{f : ι → ι₂ → α} :
(⨆ (i : ι) (j : ι₂), f i j) = ⨆ (j : ι₂) (i : ι), f i j
@[simp]
theorem
infi_infi_eq_left
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{b : β}
{f : Π (x : β), x = b → α} :
@[simp]
theorem
infi_infi_eq_right
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{b : β}
{f : Π (x : β), b = x → α} :
@[simp]
theorem
supr_supr_eq_left
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{b : β}
{f : Π (x : β), x = b → α} :
@[simp]
theorem
supr_supr_eq_right
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{b : β}
{f : Π (x : β), b = x → α} :
theorem
infi_subtype
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{p : ι → Prop}
{f : subtype p → α} :
theorem
infi_subtype'
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{p : ι → Prop}
{f : Π (i : ι), p i → α} :
@[simp]
theorem
infi_exists
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{p : ι → Prop}
{f : Exists p → α} :
@[simp]
theorem
supr_exists
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{p : ι → Prop}
{f : Exists p → α} :
theorem
supr_range
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[complete_lattice α]
{g : β → α}
{f : ι → β} :
theorem
infi_range
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[complete_lattice α]
{g : β → α}
{f : ι → β} :
theorem
Inf_image
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{s : set β}
{f : β → α} :
has_Inf.Inf (f '' s) = ⨅ (a : β) (H : a ∈ s), f a
theorem
Sup_image
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{s : set β}
{f : β → α} :
has_Sup.Sup (f '' s) = ⨆ (a : β) (H : a ∈ s), f a
theorem
infi_le_infi_of_subset
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : β → α}
{s t : set β} :
theorem
supr_le_supr_of_subset
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : β → α}
{s t : set β} :
theorem
infi_insert
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : β → α}
{s : set β}
{b : β} :
(⨅ (x : β) (H : x ∈ has_insert.insert b s), f x) = f b ⊓ ⨅ (x : β) (H : x ∈ s), f x
theorem
supr_insert
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : β → α}
{s : set β}
{b : β} :
(⨆ (x : β) (H : x ∈ has_insert.insert b s), f x) = f b ⊔ ⨆ (x : β) (H : x ∈ s), f x
theorem
infi_image
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{γ : Type u_3}
{f : β → γ}
{g : γ → α}
{t : set β} :
theorem
supr_image
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{γ : Type u_3}
{f : β → γ}
{g : γ → α}
{t : set β} :
theorem
infi_of_empty'
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
(h : ι → false)
{s : ι → α} :
theorem
supr_of_empty'
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
(h : ι → false)
{s : ι → α} :
theorem
infi_of_empty
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
(h : ¬nonempty ι)
{s : ι → α} :
theorem
supr_of_empty
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
(h : ¬nonempty ι)
{s : ι → α} :
theorem
supr_subtype
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{p : ι → Prop}
{f : subtype p → α} :
theorem
supr_subtype'
{α : Type u_1}
{ι : Sort u_4}
[complete_lattice α]
{p : ι → Prop}
{f : Π (i : ι), p i → α} :
theorem
Sup_eq_supr'
{α : Type u_1}
[complete_lattice α]
{s : set α} :
has_Sup.Sup s = ⨆ (x : ↥s), ↑x
theorem
infi_sigma
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{p : β → Type u_3}
{f : sigma p → α} :
theorem
supr_sigma
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{p : β → Type u_3}
{f : sigma p → α} :
Instances
@[instance]
Equations
- complete_lattice_Prop = {sup := bounded_distrib_lattice.sup bounded_distrib_lattice_Prop, le := bounded_distrib_lattice.le bounded_distrib_lattice_Prop, lt := bounded_distrib_lattice.lt bounded_distrib_lattice_Prop, le_refl := complete_lattice_Prop._proof_1, le_trans := complete_lattice_Prop._proof_2, lt_iff_le_not_le := complete_lattice_Prop._proof_3, le_antisymm := complete_lattice_Prop._proof_4, le_sup_left := complete_lattice_Prop._proof_5, le_sup_right := complete_lattice_Prop._proof_6, sup_le := complete_lattice_Prop._proof_7, inf := bounded_distrib_lattice.inf bounded_distrib_lattice_Prop, inf_le_left := complete_lattice_Prop._proof_8, inf_le_right := complete_lattice_Prop._proof_9, le_inf := complete_lattice_Prop._proof_10, top := bounded_distrib_lattice.top bounded_distrib_lattice_Prop, le_top := complete_lattice_Prop._proof_11, bot := bounded_distrib_lattice.bot bounded_distrib_lattice_Prop, bot_le := complete_lattice_Prop._proof_12, Sup := λ (s : set Prop), ∃ (a : Prop) (H : a ∈ s), a, Inf := λ (s : set Prop), ∀ (a : Prop), a ∈ s → a, le_Sup := complete_lattice_Prop._proof_13, Sup_le := complete_lattice_Prop._proof_14, Inf_le := complete_lattice_Prop._proof_15, le_Inf := complete_lattice_Prop._proof_16}
@[instance]
def
pi.complete_lattice
{α : Type u_1}
{β : α → Type u_2}
[Π (i : α), complete_lattice (β i)] :
complete_lattice (Π (i : α), β i)
Equations
- pi.complete_lattice = {sup := bounded_lattice.sup pi.bounded_lattice, le := bounded_lattice.le pi.bounded_lattice, lt := bounded_lattice.lt pi.bounded_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf pi.bounded_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := bounded_lattice.top pi.bounded_lattice, le_top := _, bot := bounded_lattice.bot pi.bounded_lattice, bot_le := _, Sup := has_Sup.Sup pi.has_Sup, Inf := has_Inf.Inf pi.has_Inf, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
theorem
infi_apply
{α : Type u_1}
{β : α → Type u_2}
{ι : Sort u_3}
[Π (i : α), has_Inf (β i)]
{f : ι → Π (a : α), β a}
{a : α} :
(⨅ (i : ι), f i) a = ⨅ (i : ι), f i a
theorem
supr_apply
{α : Type u_1}
{β : α → Type u_2}
{ι : Sort u_3}
[Π (i : α), has_Sup (β i)]
{f : ι → Π (a : α), β a}
{a : α} :
(⨆ (i : ι), f i) a = ⨆ (i : ι), f i a
theorem
monotone_Sup_of_monotone
{α : Type u_1}
{β : Type u_2}
[preorder α]
[complete_lattice β]
{s : set (α → β)} :
(∀ (f : α → β), f ∈ s → monotone f) → monotone (has_Sup.Sup s)
theorem
monotone_Inf_of_monotone
{α : Type u_1}
{β : Type u_2}
[preorder α]
[complete_lattice β]
{s : set (α → β)} :
(∀ (f : α → β), f ∈ s → monotone f) → monotone (has_Inf.Inf s)
@[instance]
Equations
- prod.has_Inf α β = {Inf := λ (s : set (α × β)), (has_Inf.Inf (prod.fst '' s), has_Inf.Inf (prod.snd '' s))}
@[instance]
Equations
- prod.has_Sup α β = {Sup := λ (s : set (α × β)), (has_Sup.Sup (prod.fst '' s), has_Sup.Sup (prod.snd '' s))}
@[instance]
def
prod.complete_lattice
(α : Type u_1)
(β : Type u_2)
[complete_lattice α]
[complete_lattice β] :
complete_lattice (α × β)
Equations
- prod.complete_lattice α β = {sup := bounded_lattice.sup (prod.bounded_lattice α β), le := bounded_lattice.le (prod.bounded_lattice α β), lt := bounded_lattice.lt (prod.bounded_lattice α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf (prod.bounded_lattice α β), inf_le_left := _, inf_le_right := _, le_inf := _, top := bounded_lattice.top (prod.bounded_lattice α β), le_top := _, bot := bounded_lattice.bot (prod.bounded_lattice α β), bot_le := _, Sup := has_Sup.Sup (prod.has_Sup α β), Inf := has_Inf.Inf (prod.has_Inf α β), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}