Theory of conditionally complete lattices. #
A conditionally complete lattice is a lattice in which every non-empty bounded subset s has a least upper bound and a greatest lower bound, denoted below by Sup s and Inf s. Typical examples are real, nat, int with their usual orders.
The theory is very comparable to the theory of complete lattices, except that suitable boundedness and nonemptiness assumptions have to be added to most statements. We introduce two predicates bdd_above and bdd_below to express this boundedness, prove their basic properties, and then go on to prove most useful properties of Sup and Inf in conditionally complete lattices.
To differentiate the statements between complete lattices and conditionally complete lattices, we prefix Inf and Sup in the statements by c, giving cInf and cSup. For instance, Inf_le is a statement in complete lattices ensuring Inf s ≤ x, while cInf_le is the same statement in conditionally complete lattices with an additional assumption that s is bounded below.
@[protected, instance]
Equations
@[protected, instance]
Equations
@[instance]
def
conditionally_complete_lattice.to_has_Inf
(α : Type u_4)
[self : conditionally_complete_lattice α] :
has_Inf α
@[instance]
def
conditionally_complete_lattice.to_has_Sup
(α : Type u_4)
[self : conditionally_complete_lattice α] :
has_Sup α
@[instance]
def
conditionally_complete_lattice.to_lattice
(α : Type u_4)
[self : conditionally_complete_lattice α] :
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 α → α
- Inf : set α → α
- le_cSup : ∀ (s : set α) (a : α), bdd_above s → a ∈ s → a ≤ conditionally_complete_lattice.Sup s
- cSup_le : ∀ (s : set α) (a : α), s.nonempty → a ∈ upper_bounds s → conditionally_complete_lattice.Sup s ≤ a
- cInf_le : ∀ (s : set α) (a : α), bdd_below s → a ∈ s → conditionally_complete_lattice.Inf s ≤ a
- le_cInf : ∀ (s : set α) (a : α), s.nonempty → a ∈ lower_bounds s → a ≤ conditionally_complete_lattice.Inf s
A conditionally complete lattice is a lattice in which every nonempty subset which is bounded above has a supremum, and every nonempty subset which is bounded below has an infimum. Typical examples are real numbers or natural numbers.
To differentiate the statements from the corresponding statements in (unconditional) complete lattices, we prefix Inf and Sup by a c everywhere. The same statements should hold in both worlds, sometimes with additional assumptions of nonemptiness or boundedness.
@[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 α → α
- Inf : set α → α
- le_cSup : ∀ (s : set α) (a : α), bdd_above s → a ∈ s → a ≤ conditionally_complete_linear_order.Sup s
- cSup_le : ∀ (s : set α) (a : α), s.nonempty → a ∈ upper_bounds s → conditionally_complete_linear_order.Sup s ≤ a
- cInf_le : ∀ (s : set α) (a : α), bdd_below s → a ∈ s → conditionally_complete_linear_order.Inf s ≤ a
- le_cInf : ∀ (s : set α) (a : α), s.nonempty → a ∈ lower_bounds s → a ≤ conditionally_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
- max_def : conditionally_complete_linear_order.sup = max_default . "reflexivity"
- min_def : conditionally_complete_linear_order.inf = min_default . "reflexivity"
A conditionally complete linear order is a linear order in which every nonempty subset which is bounded above has a supremum, and every nonempty subset which is bounded below has an infimum. Typical examples are real numbers or natural numbers.
To differentiate the statements from the corresponding statements in (unconditional) complete linear orders, we prefix Inf and Sup by a c everywhere. The same statements should hold in both worlds, sometimes with additional assumptions of nonemptiness or boundedness.
@[instance]
def
conditionally_complete_linear_order.to_conditionally_complete_lattice
(α : Type u_4)
[self : conditionally_complete_linear_order α] :
@[instance]
def
conditionally_complete_linear_order.to_linear_order
(α : Type u_4)
[self : conditionally_complete_linear_order α] :
@[instance]
def
conditionally_complete_linear_order_bot.to_has_bot
(α : Type u_4)
[self : conditionally_complete_linear_order_bot α] :
has_bot α
@[instance]
@[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 α → α
- Inf : set α → α
- le_cSup : ∀ (s : set α) (a : α), bdd_above s → a ∈ s → a ≤ conditionally_complete_linear_order_bot.Sup s
- cSup_le : ∀ (s : set α) (a : α), s.nonempty → a ∈ upper_bounds s → conditionally_complete_linear_order_bot.Sup s ≤ a
- cInf_le : ∀ (s : set α) (a : α), bdd_below s → a ∈ s → conditionally_complete_linear_order_bot.Inf s ≤ a
- le_cInf : ∀ (s : set α) (a : α), s.nonempty → a ∈ lower_bounds s → a ≤ conditionally_complete_linear_order_bot.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
- max_def : conditionally_complete_linear_order_bot.sup = max_default . "reflexivity"
- min_def : conditionally_complete_linear_order_bot.inf = min_default . "reflexivity"
- bot : α
- bot_le : ∀ (x : α), ⊥ ≤ x
- cSup_empty : conditionally_complete_linear_order_bot.Sup ∅ = ⊥
A conditionally complete linear order with bot is a linear order with least element, in which
every nonempty subset which is bounded above has a supremum, and every nonempty subset (necessarily
bounded below) has an infimum. A typical example is the natural numbers.
To differentiate the statements from the corresponding statements in (unconditional) complete linear orders, we prefix Inf and Sup by a c everywhere. The same statements should hold in both worlds, sometimes with additional assumptions of nonemptiness or boundedness.
@[protected, instance]
def
conditionally_complete_linear_order_bot.to_order_bot
{α : Type u_1}
[h : conditionally_complete_linear_order_bot α] :
@[protected, instance]
A complete lattice is a conditionally complete lattice, as there are no restrictions on the properties of Inf and Sup in a complete lattice.
Equations
- complete_lattice.to_conditionally_complete_lattice = {sup := complete_lattice.sup _inst_1, le := complete_lattice.le _inst_1, lt := complete_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_lattice.inf _inst_1, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup _inst_1, Inf := complete_lattice.Inf _inst_1, le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _}
@[protected, instance]
def
complete_linear_order.to_conditionally_complete_linear_order_bot
{α : Type u_1}
[complete_linear_order α] :
Equations
- complete_linear_order.to_conditionally_complete_linear_order_bot = {sup := conditionally_complete_lattice.sup complete_lattice.to_conditionally_complete_lattice, le := conditionally_complete_lattice.le complete_lattice.to_conditionally_complete_lattice, lt := conditionally_complete_lattice.lt complete_lattice.to_conditionally_complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := conditionally_complete_lattice.inf complete_lattice.to_conditionally_complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := conditionally_complete_lattice.Sup complete_lattice.to_conditionally_complete_lattice, Inf := conditionally_complete_lattice.Inf complete_lattice.to_conditionally_complete_lattice, le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _, le_total := _, decidable_le := complete_linear_order.decidable_le _inst_1, decidable_eq := complete_linear_order.decidable_eq _inst_1, decidable_lt := complete_linear_order.decidable_lt _inst_1, max_def := _, min_def := _, bot := complete_linear_order.bot _inst_1, bot_le := _, cSup_empty := _}
noncomputable
def
well_founded.conditionally_complete_linear_order_with_bot
{α : Type u_1}
[i : linear_order α]
(h : well_founded has_lt.lt)
(c : α)
(hc : c = h.min set.univ _) :
A well founded linear order is conditionally complete, with a bottom element.
Equations
- h.conditionally_complete_linear_order_with_bot c hc = {sup := max i, le := linear_order.le i, lt := linear_order.lt i, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := min i, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := λ (s : set α), dite (upper_bounds s).nonempty (λ (hs : (upper_bounds s).nonempty), h.min (upper_bounds s) hs) (λ (hs : ¬(upper_bounds s).nonempty), c), Inf := λ (s : set α), dite s.nonempty (λ (hs : s.nonempty), h.min s hs) (λ (hs : ¬s.nonempty), c), le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _, le_total := _, decidable_le := linear_order.decidable_le i, decidable_eq := linear_order.decidable_eq i, decidable_lt := linear_order.decidable_lt i, max_def := _, min_def := _, bot := c, bot_le := _, cSup_empty := _}
@[protected, instance]
Equations
- order_dual.conditionally_complete_lattice α = {sup := lattice.sup (order_dual.lattice α), le := lattice.le (order_dual.lattice α), lt := lattice.lt (order_dual.lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf (order_dual.lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := Sup (order_dual.has_Sup α), Inf := Inf (order_dual.has_Inf α), le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _}
@[protected, instance]
def
order_dual.conditionally_complete_linear_order
(α : Type u_1)
[conditionally_complete_linear_order α] :
Equations
- order_dual.conditionally_complete_linear_order α = {sup := conditionally_complete_lattice.sup (order_dual.conditionally_complete_lattice α), le := conditionally_complete_lattice.le (order_dual.conditionally_complete_lattice α), lt := conditionally_complete_lattice.lt (order_dual.conditionally_complete_lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := conditionally_complete_lattice.inf (order_dual.conditionally_complete_lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := conditionally_complete_lattice.Sup (order_dual.conditionally_complete_lattice α), Inf := conditionally_complete_lattice.Inf (order_dual.conditionally_complete_lattice α), le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _, le_total := _, decidable_le := linear_order.decidable_le (order_dual.linear_order α), decidable_eq := linear_order.decidable_eq (order_dual.linear_order α), decidable_lt := linear_order.decidable_lt (order_dual.linear_order α), max_def := _, min_def := _}
theorem
le_cSup_of_le
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{a b : α}
(_x : bdd_above s)
(hb : b ∈ s)
(h : a ≤ b) :
theorem
cInf_le_of_le
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{a b : α}
(_x : bdd_below s)
(hb : b ∈ s)
(h : b ≤ a) :
theorem
cSup_le_cSup
{α : Type u_1}
[conditionally_complete_lattice α]
{s t : set α}
(_x : bdd_above t)
(_x_1 : s.nonempty)
(h : s ⊆ t) :
theorem
cInf_le_cInf
{α : Type u_1}
[conditionally_complete_lattice α]
{s t : set α}
(_x : bdd_below t)
(_x_1 : s.nonempty)
(h : s ⊆ t) :
theorem
le_cSup_iff
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{a : α}
(h : bdd_above s)
(hs : s.nonempty) :
theorem
cInf_le_iff
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{a : α}
(h : bdd_below s)
(hs : s.nonempty) :
theorem
is_lub_cSup
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
(ne : s.nonempty)
(H : bdd_above s) :
theorem
is_lub_csupr
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
[nonempty ι]
{f : ι → α}
(H : bdd_above (set.range f)) :
theorem
is_glb_cInf
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
(ne : s.nonempty)
(H : bdd_below s) :
theorem
is_glb_cinfi
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
[nonempty ι]
{f : ι → α}
(H : bdd_below (set.range f)) :
theorem
is_lub.cSup_eq
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{a : α}
(H : is_lub s a)
(ne : s.nonempty) :
theorem
is_lub.csupr_eq
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
{a : α}
[nonempty ι]
{f : ι → α}
(H : is_lub (set.range f) a) :
(⨆ (i : ι), f i) = a
theorem
is_lub.csupr_set_eq
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{a : α}
{s : set β}
{f : β → α}
(H : is_lub (f '' s) a)
(Hne : s.nonempty) :
theorem
is_greatest.cSup_eq
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{a : α}
(H : is_greatest s a) :
A greatest element of a set is the supremum of this set.
theorem
is_greatest.Sup_mem
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{a : α}
(H : is_greatest s a) :
theorem
is_glb.cInf_eq
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{a : α}
(H : is_glb s a)
(ne : s.nonempty) :
theorem
is_glb.cinfi_eq
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
{a : α}
[nonempty ι]
{f : ι → α}
(H : is_glb (set.range f) a) :
(⨅ (i : ι), f i) = a
theorem
is_glb.cinfi_set_eq
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{a : α}
{s : set β}
{f : β → α}
(H : is_glb (f '' s) a)
(Hne : s.nonempty) :
theorem
is_least.cInf_eq
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{a : α}
(H : is_least s a) :
A least element of a set is the infimum of this set.
theorem
is_least.Inf_mem
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{a : α}
(H : is_least s a) :
theorem
subset_Icc_cInf_cSup
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
(hb : bdd_below s)
(ha : bdd_above s) :
theorem
cSup_lower_bounds_eq_cInf
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
(h : bdd_below s)
(hs : s.nonempty) :
Sup (lower_bounds s) = Inf s
theorem
cInf_upper_bounds_eq_cSup
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
(h : bdd_above s)
(hs : s.nonempty) :
Inf (upper_bounds s) = Sup s
theorem
not_mem_of_lt_cInf
{α : Type u_1}
[conditionally_complete_lattice α]
{x : α}
{s : set α}
(h : x < Inf s)
(hs : bdd_below s) :
x ∉ s
theorem
not_mem_of_cSup_lt
{α : Type u_1}
[conditionally_complete_lattice α]
{x : α}
{s : set α}
(h : Sup s < x)
(hs : bdd_above s) :
x ∉ s
theorem
cSup_eq_of_forall_le_of_forall_lt_exists_gt
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{b : α}
(_x : s.nonempty)
(_x_1 : ∀ (a : α), a ∈ s → a ≤ b)
(H : ∀ (w : α), w < b → (∃ (a : α) (H : a ∈ s), w < a)) :
Introduction rule to prove that b is the supremum of s: it suffices to check that b
is larger than all elements of s, and that this is not the case of any w<b.
See Sup_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.
theorem
cInf_eq_of_forall_ge_of_forall_gt_exists_lt
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{b : α}
(_x : s.nonempty)
(_x_1 : ∀ (a : α), a ∈ s → b ≤ a)
(H : ∀ (w : α), b < w → (∃ (a : α) (H : a ∈ s), a < w)) :
Introduction rule to prove that b is the infimum of s: it suffices to check that b
is smaller than all elements of s, and that this is not the case of any w>b.
See Inf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in complete lattices.
theorem
lt_cSup_of_lt
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{a b : α}
(_x : bdd_above s)
(_x_1 : a ∈ s)
(_x_2 : b < a) :
b < Sup s when there is an element a in s with b < a, when s is bounded above. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness above for one direction, nonemptiness and linear order for the other one), so we formulate separately the two implications, contrary to the complete_lattice case.
theorem
cInf_lt_of_lt
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{a b : α}
(_x : bdd_below s)
(_x_1 : a ∈ s)
(_x_2 : a < b) :
Inf s < b when there is an element a in s with a < b, when s is bounded below. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness below for one direction, nonemptiness and linear order for the other one), so we formulate separately the two implications, contrary to the complete_lattice case.
theorem
exists_between_of_forall_le
{α : Type u_1}
[conditionally_complete_lattice α]
{s t : set α}
(sne : s.nonempty)
(tne : t.nonempty)
(hst : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x ≤ y) :
(upper_bounds s ∩ lower_bounds t).nonempty
If all elements of a nonempty set s are less than or equal to all elements
of a nonempty set t, then there exists an element between these sets.
@[simp]
The supremum of a singleton is the element of the singleton
@[simp]
The infimum of a singleton is the element of the singleton
theorem
cInf_le_cSup
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
(hb : bdd_below s)
(ha : bdd_above s)
(ne : s.nonempty) :
If a set is bounded below and above, and nonempty, its infimum is less than or equal to its supremum.
theorem
cSup_union
{α : Type u_1}
[conditionally_complete_lattice α]
{s t : set α}
(hs : bdd_above s)
(sne : s.nonempty)
(ht : bdd_above t)
(tne : t.nonempty) :
The sup of a union of two sets is the max of the suprema of each subset, under the assumptions that all sets are bounded above and nonempty.
theorem
cInf_union
{α : Type u_1}
[conditionally_complete_lattice α]
{s t : set α}
(hs : bdd_below s)
(sne : s.nonempty)
(ht : bdd_below t)
(tne : t.nonempty) :
The inf of a union of two sets is the min of the infima of each subset, under the assumptions that all sets are bounded below and nonempty.
theorem
cSup_inter_le
{α : Type u_1}
[conditionally_complete_lattice α]
{s t : set α}
(_x : bdd_above s)
(_x_1 : bdd_above t)
(hst : (s ∩ t).nonempty) :
The supremum of an intersection of two sets is bounded by the minimum of the suprema of each set, if all sets are bounded above and nonempty.
theorem
le_cInf_inter
{α : Type u_1}
[conditionally_complete_lattice α]
{s t : set α}
(_x : bdd_below s)
(_x_1 : bdd_below t)
(hst : (s ∩ t).nonempty) :
The infimum of an intersection of two sets is bounded below by the maximum of the infima of each set, if all sets are bounded below and nonempty.
@[simp]
theorem
cInf_Ioc
{α : Type u_1}
[conditionally_complete_lattice α]
{a b : α}
[densely_ordered α]
(h : a < b) :
@[simp]
theorem
cInf_Ioi
{α : Type u_1}
[conditionally_complete_lattice α]
{a : α}
[no_max_order α]
[densely_ordered α] :
@[simp]
theorem
cInf_Ioo
{α : Type u_1}
[conditionally_complete_lattice α]
{a b : α}
[densely_ordered α]
(h : a < b) :
@[simp]
theorem
cSup_Ico
{α : Type u_1}
[conditionally_complete_lattice α]
{a b : α}
[densely_ordered α]
(h : a < b) :
@[simp]
theorem
cSup_Iio
{α : Type u_1}
[conditionally_complete_lattice α]
{a : α}
[no_min_order α]
[densely_ordered α] :
@[simp]
theorem
cSup_Ioo
{α : Type u_1}
[conditionally_complete_lattice α]
{a b : α}
[densely_ordered α]
(h : a < b) :
theorem
le_csupr_of_le
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
{a : α}
{f : ι → α}
(H : bdd_above (set.range f))
(c : ι)
(h : a ≤ f c) :
theorem
csupr_mono
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
{f g : ι → α}
(B : bdd_above (set.range g))
(H : ∀ (x : ι), f x ≤ g x) :
The indexed supremum of two functions are comparable if the functions are pointwise comparable
theorem
le_csupr_set
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{f : β → α}
{s : set β}
(H : bdd_above (f '' s))
{c : β}
(hc : c ∈ s) :
theorem
cinfi_mono
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
{f g : ι → α}
(B : bdd_below (set.range f))
(H : ∀ (x : ι), f x ≤ g x) :
The indexed infimum of two functions are comparable if the functions are pointwise comparable
theorem
cinfi_le_of_le
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
{a : α}
{f : ι → α}
(H : bdd_below (set.range f))
(c : ι)
(h : f c ≤ a) :
theorem
cinfi_set_le
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{f : β → α}
{s : set β}
(H : bdd_below (f '' s))
{c : β}
(hc : c ∈ s) :
@[simp]
theorem
csupr_const
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
[hι : nonempty ι]
{a : α} :
(⨆ (b : ι), a) = a
@[simp]
theorem
cinfi_const
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
[hι : nonempty ι]
{a : α} :
(⨅ (b : ι), a) = a
theorem
supr_unique
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
[unique ι]
{s : ι → α} :
theorem
infi_unique
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
[unique ι]
{s : ι → α} :
@[simp]
theorem
csupr_pos
{α : Type u_1}
[conditionally_complete_lattice α]
{p : Prop}
{f : p → α}
(hp : p) :
(⨆ (h : p), f h) = f hp
@[simp]
theorem
cinfi_pos
{α : Type u_1}
[conditionally_complete_lattice α]
{p : Prop}
{f : p → α}
(hp : p) :
(⨅ (h : p), f h) = f hp
theorem
csupr_eq_of_forall_le_of_forall_lt_exists_gt
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
{b : α}
[nonempty ι]
{f : ι → α}
(h₁ : ∀ (i : ι), f i ≤ b)
(h₂ : ∀ (w : α), w < b → (∃ (i : ι), w < f i)) :
(⨆ (i : ι), f i) = b
Introduction rule to prove that b is the supremum of f: it suffices to check that b
is larger than f i for all i, and that this is not the case of any w<b.
See supr_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.
theorem
cinfi_eq_of_forall_ge_of_forall_gt_exists_lt
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_lattice α]
{b : α}
[nonempty ι]
{f : ι → α}
(h₁ : ∀ (i : ι), b ≤ f i)
(h₂ : ∀ (w : α), b < w → (∃ (i : ι), f i < w)) :
(⨅ (i : ι), f i) = b
Introduction rule to prove that b is the infimum of f: it suffices to check that b
is smaller than f i for all i, and that this is not the case of any w>b.
See infi_eq_of_forall_ge_of_forall_gt_exists_lt for a version in complete lattices.
theorem
monotone.csupr_mem_Inter_Icc_of_antitone
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
[semilattice_sup β]
{f g : β → α}
(hf : monotone f)
(hg : antitone g)
(h : f ≤ g) :
Nested intervals lemma: if f is a monotone sequence, g is an antitone sequence, and
f n ≤ g n for all n, then ⨆ n, f n belongs to all the intervals [f n, g n].
theorem
csupr_mem_Inter_Icc_of_antitone_Icc
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
[semilattice_sup β]
{f g : β → α}
(h : antitone (λ (n : β), set.Icc (f n) (g n)))
(h' : ∀ (n : β), f n ≤ g n) :
Nested intervals lemma: if [f n, g n] is an antitone sequence of nonempty
closed intervals, then ⨆ n, f n belongs to all the intervals [f n, g n].
theorem
finset.nonempty.sup'_eq_cSup_image
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{s : finset β}
(hs : s.nonempty)
(f : β → α) :
theorem
finset.nonempty.sup'_id_eq_cSup
{α : Type u_1}
[conditionally_complete_lattice α]
{s : finset α}
(hs : s.nonempty) :
theorem
cSup_eq_of_is_forall_le_of_forall_le_imp_ge
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
{b : α}
(_x : s.nonempty)
(h_is_ub : ∀ (a : α), a ∈ s → a ≤ b)
(h_b_le_ub : ∀ (ub : α), (∀ (a : α), a ∈ s → a ≤ ub) → b ≤ ub) :
Introduction rule to prove that b is the supremum of s: it suffices to check that
- b is an upper bound
- every other upper bound b' satisfies b ≤ b'.
@[protected, instance]
def
pi.conditionally_complete_lattice
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), conditionally_complete_lattice (α i)] :
conditionally_complete_lattice (Π (i : ι), α i)
Equations
- pi.conditionally_complete_lattice = {sup := lattice.sup pi.lattice, le := lattice.le pi.lattice, lt := lattice.lt pi.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf pi.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := Sup pi.has_Sup, Inf := Inf pi.has_Inf, le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _}
theorem
finset.nonempty.cSup_eq_max'
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : finset α}
(h : s.nonempty) :
theorem
finset.nonempty.cInf_eq_min'
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : finset α}
(h : s.nonempty) :
theorem
finset.nonempty.cSup_mem
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : finset α}
(h : s.nonempty) :
theorem
finset.nonempty.cInf_mem
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : finset α}
(h : s.nonempty) :
theorem
set.nonempty.cSup_mem
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : set α}
(h : s.nonempty)
(hs : s.finite) :
theorem
set.nonempty.cInf_mem
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : set α}
(h : s.nonempty)
(hs : s.finite) :
theorem
exists_lt_of_lt_cSup
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : set α}
{b : α}
(hs : s.nonempty)
(hb : b < Sup s) :
When b < Sup s, there is an element a in s with b < a, if s is nonempty and the order is a linear order.
theorem
exists_lt_of_lt_csupr
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_linear_order α]
{b : α}
[nonempty ι]
{f : ι → α}
(h : b < supr f) :
∃ (i : ι), b < f i
Indexed version of the above lemma exists_lt_of_lt_cSup.
When b < supr f, there is an element i such that b < f i.
theorem
exists_lt_of_cInf_lt
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : set α}
{b : α}
(hs : s.nonempty)
(hb : Inf s < b) :
When Inf s < b, there is an element a in s with a < b, if s is nonempty and the order is a linear order.
theorem
exists_lt_of_cinfi_lt
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_linear_order α]
{a : α}
[nonempty ι]
{f : ι → α}
(h : infi f < a) :
∃ (i : ι), f i < a
Indexed version of the above lemma exists_lt_of_cInf_lt
When infi f < a, there is an element i such that f i < a.
theorem
Inf_eq_argmin_on
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : set α}
[is_well_order α has_lt.lt]
(hs : s.nonempty) :
Inf s = function.argmin_on id is_well_order.wf s hs
theorem
is_least_Inf
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : set α}
[is_well_order α has_lt.lt]
(hs : s.nonempty) :
theorem
le_cInf_iff'
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : set α}
{b : α}
[is_well_order α has_lt.lt]
(hs : s.nonempty) :
b ≤ Inf s ↔ b ∈ lower_bounds s
theorem
Inf_mem
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : set α}
[is_well_order α has_lt.lt]
(hs : s.nonempty) :
Lemmas about a conditionally complete linear order with bottom element #
In this case we have Sup ∅ = ⊥, so we can drop some nonempty/set.nonempty assumptions.
@[simp]
@[simp]
theorem
csupr_of_empty
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_linear_order_bot α]
[is_empty ι]
(f : ι → α) :
@[simp]
theorem
is_lub_cSup'
{α : Type u_1}
[conditionally_complete_linear_order_bot α]
{s : set α}
(hs : bdd_above s) :
theorem
cSup_le_iff'
{α : Type u_1}
[conditionally_complete_linear_order_bot α]
{s : set α}
(hs : bdd_above s)
{a : α} :
theorem
cSup_le'
{α : Type u_1}
[conditionally_complete_linear_order_bot α]
{s : set α}
{a : α}
(h : a ∈ upper_bounds s) :
theorem
le_cSup_iff'
{α : Type u_1}
[conditionally_complete_linear_order_bot α]
{s : set α}
{a : α}
(h : bdd_above s) :
theorem
le_cInf_iff''
{α : Type u_1}
[conditionally_complete_linear_order_bot α]
{s : set α}
{a : α}
(ne : s.nonempty) :
theorem
exists_lt_of_lt_cSup'
{α : Type u_1}
[conditionally_complete_linear_order_bot α]
{s : set α}
{a : α}
(h : a < Sup s) :
theorem
csupr_le_iff'
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_linear_order_bot α]
{f : ι → α}
(h : bdd_above (set.range f))
{a : α} :
theorem
csupr_le'
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_linear_order_bot α]
{f : ι → α}
{a : α}
(h : ∀ (i : ι), f i ≤ a) :
(⨆ (i : ι), f i) ≤ a
theorem
exists_lt_of_lt_csupr'
{α : Type u_1}
{ι : Sort u_3}
[conditionally_complete_linear_order_bot α]
{f : ι → α}
{a : α}
(h : a < ⨆ (i : ι), f i) :
∃ (i : ι), a < f i
theorem
with_top.is_lub_Sup'
{β : Type u_1}
[conditionally_complete_lattice β]
{s : set (with_top β)}
(hs : s.nonempty) :
The Sup of a non-empty set is its least upper bound for a conditionally complete lattice with a top.
theorem
with_top.is_lub_Sup
{α : Type u_1}
[conditionally_complete_linear_order_bot α]
(s : set (with_top α)) :
theorem
with_top.is_glb_Inf'
{β : Type u_1}
[conditionally_complete_lattice β]
{s : set (with_top β)}
(hs : bdd_below s) :
The Inf of a bounded-below set is its greatest lower bound for a conditionally complete lattice with a top.
theorem
with_top.is_glb_Inf
{α : Type u_1}
[conditionally_complete_linear_order_bot α]
(s : set (with_top α)) :
@[protected, instance]
noncomputable
def
with_top.complete_linear_order
{α : Type u_1}
[conditionally_complete_linear_order_bot α] :
Equations
- with_top.complete_linear_order = {sup := lattice.sup with_top.lattice, le := linear_order.le with_top.linear_order, lt := linear_order.lt with_top.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf with_top.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := Sup with_top.has_Sup, le_Sup := _, Sup_le := _, Inf := Inf with_top.has_Inf, Inf_le := _, le_Inf := _, top := order_top.top with_top.order_top, bot := order_bot.bot with_top.order_bot, le_top := _, bot_le := _, le_total := _, decidable_le := linear_order.decidable_le with_top.linear_order, decidable_eq := linear_order.decidable_eq with_top.linear_order, decidable_lt := linear_order.decidable_lt with_top.linear_order, max_def := _, min_def := _}
theorem
with_top.coe_Sup
{α : Type u_1}
[conditionally_complete_linear_order_bot α]
{s : set α}
(hb : bdd_above s) :
theorem
with_top.coe_Inf
{α : Type u_1}
[conditionally_complete_linear_order_bot α]
{s : set α}
(hs : s.nonempty) :
A monotone function into a conditionally complete lattice preserves the ordering properties of
Sup and Inf.
theorem
monotone.cSup_image_le
{α : Type u_1}
{β : Type u_2}
[preorder α]
[conditionally_complete_lattice β]
{f : α → β}
(h_mono : monotone f)
{s : set α}
(hs : s.nonempty)
{B : α}
(hB : B ∈ upper_bounds s) :
theorem
monotone.le_cInf_image
{α : Type u_1}
{β : Type u_2}
[preorder α]
[conditionally_complete_lattice β]
{f : α → β}
(h_mono : monotone f)
{s : set α}
(hs : s.nonempty)
{B : α}
(hB : B ∈ lower_bounds s) :
theorem
galois_connection.l_cSup
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{s : set α}
(hne : s.nonempty)
(hbdd : bdd_above s) :
theorem
galois_connection.l_cSup'
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{s : set α}
(hne : s.nonempty)
(hbdd : bdd_above s) :
theorem
galois_connection.l_csupr
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
[nonempty ι]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{f : ι → α}
(hf : bdd_above (set.range f)) :
l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)
theorem
galois_connection.l_csupr_set
{α : Type u_1}
{β : Type u_2}
{γ : Type u_4}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{s : set γ}
{f : γ → α}
(hf : bdd_above (f '' s))
(hne : s.nonempty) :
theorem
galois_connection.u_cInf
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{s : set β}
(hne : s.nonempty)
(hbdd : bdd_below s) :
theorem
galois_connection.u_cInf'
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{s : set β}
(hne : s.nonempty)
(hbdd : bdd_below s) :
theorem
galois_connection.u_cinfi
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
[nonempty ι]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{f : ι → β}
(hf : bdd_below (set.range f)) :
u (⨅ (i : ι), f i) = ⨅ (i : ι), u (f i)
theorem
galois_connection.u_cinfi_set
{α : Type u_1}
{β : Type u_2}
{γ : Type u_4}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{s : set γ}
{f : γ → β}
(hf : bdd_below (f '' s))
(hne : s.nonempty) :
theorem
order_iso.map_cSup
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
(e : α ≃o β)
{s : set α}
(hne : s.nonempty)
(hbdd : bdd_above s) :
theorem
order_iso.map_cSup'
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
(e : α ≃o β)
{s : set α}
(hne : s.nonempty)
(hbdd : bdd_above s) :
theorem
order_iso.map_csupr
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
[nonempty ι]
(e : α ≃o β)
{f : ι → α}
(hf : bdd_above (set.range f)) :
theorem
order_iso.map_cInf
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
(e : α ≃o β)
{s : set α}
(hne : s.nonempty)
(hbdd : bdd_below s) :
theorem
order_iso.map_cInf'
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
(e : α ≃o β)
{s : set α}
(hne : s.nonempty)
(hbdd : bdd_below s) :
theorem
order_iso.map_cinfi
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
[nonempty ι]
(e : α ≃o β)
{f : ι → α}
(hf : bdd_below (set.range f)) :
Relation between Sup / Inf and finset.sup' / finset.inf' #
Like the Sup of a conditionally_complete_lattice, finset.sup' also requires the set to be
non-empty. As a result, we can translate between the two.
theorem
finset.sup'_eq_cSup_image
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice β]
(s : finset α)
(H : s.nonempty)
(f : α → β) :
theorem
finset.inf'_eq_cInf_image
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice β]
(s : finset α)
(H : s.nonempty)
(f : α → β) :
theorem
finset.sup'_id_eq_cSup
{α : Type u_1}
[conditionally_complete_lattice α]
(s : finset α)
(H : s.nonempty) :
theorem
finset.inf'_id_eq_cInf
{α : Type u_1}
[conditionally_complete_lattice α]
(s : finset α)
(H : s.nonempty) :
Complete lattice structure on with_top (with_bot α) #
If α is a conditionally_complete_lattice, then we show that with_top α and with_bot α
also inherit the structure of conditionally complete lattices. Furthermore, we show
that with_top (with_bot α) naturally inherits the structure of a complete lattice. Note that
for α a conditionally complete lattice, Sup and Inf both return junk values
for sets which are empty or unbounded. The extension of Sup to with_top α fixes
the unboundedness problem and the extension to with_bot α fixes the problem with
the empty set.
This result can be used to show that the extended reals [-∞, ∞] are a complete lattice.
@[protected, instance]
noncomputable
def
with_top.conditionally_complete_lattice
{α : Type u_1}
[conditionally_complete_lattice α] :
Adding a top element to a conditionally complete lattice gives a conditionally complete lattice
Equations
- with_top.conditionally_complete_lattice = {sup := lattice.sup with_top.lattice, le := lattice.le with_top.lattice, lt := lattice.lt with_top.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf with_top.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := Sup with_top.has_Sup, Inf := Inf with_top.has_Inf, le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _}
@[protected, instance]
noncomputable
def
with_bot.conditionally_complete_lattice
{α : Type u_1}
[conditionally_complete_lattice α] :
Adding a bottom element to a conditionally complete lattice gives a conditionally complete lattice
Equations
- with_bot.conditionally_complete_lattice = {sup := lattice.sup with_bot.lattice, le := lattice.le with_bot.lattice, lt := lattice.lt with_bot.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf with_bot.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := Sup with_bot.has_Sup, Inf := Inf with_bot.has_Inf, le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _}
@[protected, instance]
noncomputable
def
with_top.with_bot.complete_lattice
{α : Type u_1}
[conditionally_complete_lattice α] :
complete_lattice (with_top (with_bot α))
Equations
- with_top.with_bot.complete_lattice = {sup := lattice.sup with_top.lattice, le := lattice.le with_top.lattice, lt := lattice.lt with_top.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf with_top.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := Sup with_top.has_Sup, le_Sup := _, Sup_le := _, Inf := Inf with_top.has_Inf, Inf_le := _, le_Inf := _, top := bounded_order.top with_top.bounded_order, bot := bounded_order.bot with_top.bounded_order, le_top := _, bot_le := _}
@[protected, instance]
noncomputable
def
with_top.with_bot.complete_linear_order
{α : Type u_1}
[conditionally_complete_linear_order α] :
Equations
- with_top.with_bot.complete_linear_order = {sup := complete_lattice.sup with_top.with_bot.complete_lattice, le := complete_lattice.le with_top.with_bot.complete_lattice, lt := complete_lattice.lt with_top.with_bot.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 with_top.with_bot.complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup with_top.with_bot.complete_lattice, le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf with_top.with_bot.complete_lattice, Inf_le := _, le_Inf := _, top := complete_lattice.top with_top.with_bot.complete_lattice, bot := complete_lattice.bot with_top.with_bot.complete_lattice, le_top := _, bot_le := _, le_total := _, decidable_le := linear_order.decidable_le with_top.linear_order, decidable_eq := linear_order.decidable_eq with_top.linear_order, decidable_lt := linear_order.decidable_lt with_top.linear_order, max_def := _, min_def := _}
theorem
le_add_cinfi
{α : Type u_1}
{ι : Sort u_3}
[nonempty ι]
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
{a g : α}
{h : ι → α}
(H : ∀ (j : ι), a ≤ g + h j) :
theorem
le_mul_cinfi
{α : Type u_1}
{ι : Sort u_3}
[nonempty ι]
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
{a g : α}
{h : ι → α}
(H : ∀ (j : ι), a ≤ g * h j) :
theorem
mul_csupr_le
{α : Type u_1}
{ι : Sort u_3}
[nonempty ι]
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
{a g : α}
{h : ι → α}
(H : ∀ (j : ι), g * h j ≤ a) :
theorem
add_csupr_le
{α : Type u_1}
{ι : Sort u_3}
[nonempty ι]
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
{a g : α}
{h : ι → α}
(H : ∀ (j : ι), g + h j ≤ a) :
theorem
le_cinfi_add
{α : Type u_1}
{ι : Sort u_3}
[nonempty ι]
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a : α}
{g : ι → α}
{h : α}
(H : ∀ (i : ι), a ≤ g i + h) :
theorem
le_cinfi_mul
{α : Type u_1}
{ι : Sort u_3}
[nonempty ι]
[conditionally_complete_lattice α]
[group α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a : α}
{g : ι → α}
{h : α}
(H : ∀ (i : ι), a ≤ (g i) * h) :
theorem
csupr_mul_le
{α : Type u_1}
{ι : Sort u_3}
[nonempty ι]
[conditionally_complete_lattice α]
[group α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a : α}
{g : ι → α}
{h : α}
(H : ∀ (i : ι), (g i) * h ≤ a) :
theorem
csupr_add_le
{α : Type u_1}
{ι : Sort u_3}
[nonempty ι]
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a : α}
{g : ι → α}
{h : α}
(H : ∀ (i : ι), g i + h ≤ a) :
theorem
le_cinfi_mul_cinfi
{α : Type u_1}
{ι : Sort u_3}
[nonempty ι]
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a : α}
{g h : ι → α}
(H : ∀ (i j : ι), a ≤ (g i) * h j) :
theorem
le_cinfi_add_cinfi
{α : Type u_1}
{ι : Sort u_3}
[nonempty ι]
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a : α}
{g h : ι → α}
(H : ∀ (i j : ι), a ≤ g i + h j) :
theorem
csupr_mul_csupr_le
{α : Type u_1}
{ι : Sort u_3}
[nonempty ι]
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a : α}
{g h : ι → α}
(H : ∀ (i j : ι), (g i) * h j ≤ a) :
theorem
csupr_add_csupr_le
{α : Type u_1}
{ι : Sort u_3}
[nonempty ι]
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a : α}
{g h : ι → α}
(H : ∀ (i j : ι), g i + h j ≤ a) :