Upper/lower bounds in ordered monoids and groups #
In this file we prove a few facts like “-s is bounded above iff s is bounded below”
(bdd_above_neg).
@[simp]
theorem
bdd_above_neg
{G : Type u_1}
[add_group G]
[preorder G]
[covariant_class G G has_add.add has_le.le]
[covariant_class G G (function.swap has_add.add) has_le.le]
{s : set G} :
@[simp]
theorem
bdd_above_inv
{G : Type u_1}
[group G]
[preorder G]
[covariant_class G G has_mul.mul has_le.le]
[covariant_class G G (function.swap has_mul.mul) has_le.le]
{s : set G} :
@[simp]
theorem
bdd_below_neg
{G : Type u_1}
[add_group G]
[preorder G]
[covariant_class G G has_add.add has_le.le]
[covariant_class G G (function.swap has_add.add) has_le.le]
{s : set G} :
@[simp]
theorem
bdd_below_inv
{G : Type u_1}
[group G]
[preorder G]
[covariant_class G G has_mul.mul has_le.le]
[covariant_class G G (function.swap has_mul.mul) has_le.le]
{s : set G} :
theorem
bdd_above.neg
{G : Type u_1}
[add_group G]
[preorder G]
[covariant_class G G has_add.add has_le.le]
[covariant_class G G (function.swap has_add.add) has_le.le]
{s : set G}
(h : bdd_above s) :
theorem
bdd_above.inv
{G : Type u_1}
[group G]
[preorder G]
[covariant_class G G has_mul.mul has_le.le]
[covariant_class G G (function.swap has_mul.mul) has_le.le]
{s : set G}
(h : bdd_above s) :
theorem
bdd_below.inv
{G : Type u_1}
[group G]
[preorder G]
[covariant_class G G has_mul.mul has_le.le]
[covariant_class G G (function.swap has_mul.mul) has_le.le]
{s : set G}
(h : bdd_below s) :
theorem
bdd_below.neg
{G : Type u_1}
[add_group G]
[preorder G]
[covariant_class G G has_add.add has_le.le]
[covariant_class G G (function.swap has_add.add) has_le.le]
{s : set G}
(h : bdd_below s) :
@[simp]
theorem
is_lub_neg
{G : Type u_1}
[add_group G]
[preorder G]
[covariant_class G G has_add.add has_le.le]
[covariant_class G G (function.swap has_add.add) has_le.le]
{s : set G}
{a : G} :
@[simp]
theorem
is_lub_inv
{G : Type u_1}
[group G]
[preorder G]
[covariant_class G G has_mul.mul has_le.le]
[covariant_class G G (function.swap has_mul.mul) has_le.le]
{s : set G}
{a : G} :
theorem
is_lub_neg'
{G : Type u_1}
[add_group G]
[preorder G]
[covariant_class G G has_add.add has_le.le]
[covariant_class G G (function.swap has_add.add) has_le.le]
{s : set G}
{a : G} :
theorem
is_lub_inv'
{G : Type u_1}
[group G]
[preorder G]
[covariant_class G G has_mul.mul has_le.le]
[covariant_class G G (function.swap has_mul.mul) has_le.le]
{s : set G}
{a : G} :
theorem
is_glb.inv
{G : Type u_1}
[group G]
[preorder G]
[covariant_class G G has_mul.mul has_le.le]
[covariant_class G G (function.swap has_mul.mul) has_le.le]
{s : set G}
{a : G}
(h : is_glb s a) :
theorem
is_glb.neg
{G : Type u_1}
[add_group G]
[preorder G]
[covariant_class G G has_add.add has_le.le]
[covariant_class G G (function.swap has_add.add) has_le.le]
{s : set G}
{a : G}
(h : is_glb s a) :
@[simp]
theorem
is_glb_neg
{G : Type u_1}
[add_group G]
[preorder G]
[covariant_class G G has_add.add has_le.le]
[covariant_class G G (function.swap has_add.add) has_le.le]
{s : set G}
{a : G} :
@[simp]
theorem
is_glb_inv
{G : Type u_1}
[group G]
[preorder G]
[covariant_class G G has_mul.mul has_le.le]
[covariant_class G G (function.swap has_mul.mul) has_le.le]
{s : set G}
{a : G} :
theorem
is_glb_neg'
{G : Type u_1}
[add_group G]
[preorder G]
[covariant_class G G has_add.add has_le.le]
[covariant_class G G (function.swap has_add.add) has_le.le]
{s : set G}
{a : G} :
theorem
is_glb_inv'
{G : Type u_1}
[group G]
[preorder G]
[covariant_class G G has_mul.mul has_le.le]
[covariant_class G G (function.swap has_mul.mul) has_le.le]
{s : set G}
{a : G} :
theorem
is_lub.inv
{G : Type u_1}
[group G]
[preorder G]
[covariant_class G G has_mul.mul has_le.le]
[covariant_class G G (function.swap has_mul.mul) has_le.le]
{s : set G}
{a : G}
(h : is_lub s a) :
theorem
is_lub.neg
{G : Type u_1}
[add_group G]
[preorder G]
[covariant_class G G has_add.add has_le.le]
[covariant_class G G (function.swap has_add.add) has_le.le]
{s : set G}
{a : G}
(h : is_lub s a) :
theorem
add_mem_upper_bounds_add
{M : Type u_1}
[has_add M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
[covariant_class M M (function.swap has_add.add) has_le.le]
{s t : set M}
{a b : M}
(ha : a ∈ upper_bounds s)
(hb : b ∈ upper_bounds t) :
a + b ∈ upper_bounds (s + t)
theorem
mul_mem_upper_bounds_mul
{M : Type u_1}
[has_mul M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
{s t : set M}
{a b : M}
(ha : a ∈ upper_bounds s)
(hb : b ∈ upper_bounds t) :
a * b ∈ upper_bounds (s * t)
theorem
subset_upper_bounds_add
{M : Type u_1}
[has_add M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
[covariant_class M M (function.swap has_add.add) has_le.le]
(s t : set M) :
upper_bounds s + upper_bounds t ⊆ upper_bounds (s + t)
theorem
subset_upper_bounds_mul
{M : Type u_1}
[has_mul M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
(s t : set M) :
(upper_bounds s) * upper_bounds t ⊆ upper_bounds (s * t)
theorem
mul_mem_lower_bounds_mul
{M : Type u_1}
[has_mul M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
{s t : set M}
{a b : M}
(ha : a ∈ lower_bounds s)
(hb : b ∈ lower_bounds t) :
a * b ∈ lower_bounds (s * t)
theorem
add_mem_lower_bounds_add
{M : Type u_1}
[has_add M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
[covariant_class M M (function.swap has_add.add) has_le.le]
{s t : set M}
{a b : M}
(ha : a ∈ lower_bounds s)
(hb : b ∈ lower_bounds t) :
a + b ∈ lower_bounds (s + t)
theorem
subset_lower_bounds_mul
{M : Type u_1}
[has_mul M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
(s t : set M) :
(lower_bounds s) * lower_bounds t ⊆ lower_bounds (s * t)
theorem
subset_lower_bounds_add
{M : Type u_1}
[has_add M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
[covariant_class M M (function.swap has_add.add) has_le.le]
(s t : set M) :
lower_bounds s + lower_bounds t ⊆ lower_bounds (s + t)
theorem
bdd_above.add
{M : Type u_1}
[has_add M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
[covariant_class M M (function.swap has_add.add) has_le.le]
{s t : set M}
(hs : bdd_above s)
(ht : bdd_above t) :
theorem
bdd_above.mul
{M : Type u_1}
[has_mul M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
{s t : set M}
(hs : bdd_above s)
(ht : bdd_above t) :
theorem
bdd_below.add
{M : Type u_1}
[has_add M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
[covariant_class M M (function.swap has_add.add) has_le.le]
{s t : set M}
(hs : bdd_below s)
(ht : bdd_below t) :
theorem
bdd_below.mul
{M : Type u_1}
[has_mul M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
{s t : set M}
(hs : bdd_below s)
(ht : bdd_below t) :
theorem
csupr_add
{ι : Type u_1}
{G : Type u_2}
[add_group G]
[conditionally_complete_lattice G]
[covariant_class G G (function.swap has_add.add) has_le.le]
[nonempty ι]
{f : ι → G}
(hf : bdd_above (set.range f))
(a : G) :
theorem
csupr_mul
{ι : Type u_1}
{G : Type u_2}
[group G]
[conditionally_complete_lattice G]
[covariant_class G G (function.swap has_mul.mul) has_le.le]
[nonempty ι]
{f : ι → G}
(hf : bdd_above (set.range f))
(a : G) :
theorem
csupr_div
{ι : Type u_1}
{G : Type u_2}
[group G]
[conditionally_complete_lattice G]
[covariant_class G G (function.swap has_mul.mul) has_le.le]
[nonempty ι]
{f : ι → G}
(hf : bdd_above (set.range f))
(a : G) :
theorem
csupr_sub
{ι : Type u_1}
{G : Type u_2}
[add_group G]
[conditionally_complete_lattice G]
[covariant_class G G (function.swap has_add.add) has_le.le]
[nonempty ι]
{f : ι → G}
(hf : bdd_above (set.range f))
(a : G) :
theorem
add_csupr
{ι : Type u_1}
{G : Type u_2}
[add_group G]
[conditionally_complete_lattice G]
[covariant_class G G has_add.add has_le.le]
[nonempty ι]
{f : ι → G}
(hf : bdd_above (set.range f))
(a : G) :
theorem
mul_csupr
{ι : Type u_1}
{G : Type u_2}
[group G]
[conditionally_complete_lattice G]
[covariant_class G G has_mul.mul has_le.le]
[nonempty ι]
{f : ι → G}
(hf : bdd_above (set.range f))
(a : G) :