algebra.bounds

# 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] {s : set G} :
@[simp]
theorem bdd_above_inv {G : Type u_1} [group G] [preorder G] {s : set G} :
@[simp]
theorem bdd_below_neg {G : Type u_1} [add_group G] [preorder G] {s : set G} :
@[simp]
theorem bdd_below_inv {G : Type u_1} [group G] [preorder G] {s : set G} :
theorem bdd_above.neg {G : Type u_1} [add_group G] [preorder G] {s : set G} (h : bdd_above s) :
theorem bdd_above.inv {G : Type u_1} [group G] [preorder G] {s : set G} (h : bdd_above s) :
theorem bdd_below.inv {G : Type u_1} [group G] [preorder G] {s : set G} (h : bdd_below s) :
theorem bdd_below.neg {G : Type u_1} [add_group G] [preorder G] {s : set G} (h : bdd_below s) :
@[simp]
theorem is_lub_neg {G : Type u_1} [add_group G] [preorder G] {s : set G} {a : G} :
is_lub (-s) a (-a)
@[simp]
theorem is_lub_inv {G : Type u_1} [group G] [preorder G] {s : set G} {a : G} :
theorem is_lub_neg' {G : Type u_1} [add_group G] [preorder G] {s : set G} {a : G} :
is_lub (-s) (-a) a
theorem is_lub_inv' {G : Type u_1} [group G] [preorder G] {s : set G} {a : G} :
theorem is_glb.inv {G : Type u_1} [group G] [preorder G] {s : set G} {a : G} (h : a) :
theorem is_glb.neg {G : Type u_1} [add_group G] [preorder G] {s : set G} {a : G} (h : a) :
is_lub (-s) (-a)
@[simp]
theorem is_glb_neg {G : Type u_1} [add_group G] [preorder G] {s : set G} {a : G} :
is_glb (-s) a (-a)
@[simp]
theorem is_glb_inv {G : Type u_1} [group G] [preorder G] {s : set G} {a : G} :
theorem is_glb_neg' {G : Type u_1} [add_group G] [preorder G] {s : set G} {a : G} :
is_glb (-s) (-a) a
theorem is_glb_inv' {G : Type u_1} [group G] [preorder G] {s : set G} {a : G} :
theorem is_lub.inv {G : Type u_1} [group G] [preorder G] {s : set G} {a : G} (h : a) :
theorem is_lub.neg {G : Type u_1} [add_group G] [preorder G] {s : set G} {a : G} (h : a) :
is_glb (-s) (-a)
theorem add_mem_upper_bounds_add {M : Type u_1} [has_add M] [preorder M] {s t : set M} {a b : M} (ha : a ) (hb : b ) :
a + b upper_bounds (s + t)
theorem mul_mem_upper_bounds_mul {M : Type u_1} [has_mul M] [preorder M] {s t : set M} {a b : M} (ha : a ) (hb : b ) :
a * b upper_bounds (s * t)
theorem subset_upper_bounds_add {M : Type u_1} [has_add M] [preorder M] (s t : set M) :
theorem subset_upper_bounds_mul {M : Type u_1} [has_mul M] [preorder M] (s t : set M) :
theorem mul_mem_lower_bounds_mul {M : Type u_1} [has_mul M] [preorder M] {s t : set M} {a b : M} (ha : a ) (hb : b ) :
a * b lower_bounds (s * t)
theorem add_mem_lower_bounds_add {M : Type u_1} [has_add M] [preorder M] {s t : set M} {a b : M} (ha : a ) (hb : b ) :
a + b lower_bounds (s + t)
theorem subset_lower_bounds_mul {M : Type u_1} [has_mul M] [preorder M] (s t : set M) :
theorem subset_lower_bounds_add {M : Type u_1} [has_add M] [preorder M] (s t : set M) :
theorem bdd_above.add {M : Type u_1} [has_add M] [preorder M] {s t : set M} (hs : bdd_above s) (ht : bdd_above t) :
bdd_above (s + t)
theorem bdd_above.mul {M : Type u_1} [has_mul M] [preorder M] {s t : set M} (hs : bdd_above s) (ht : bdd_above t) :
bdd_above (s * t)
theorem bdd_below.add {M : Type u_1} [has_add M] [preorder M] {s t : set M} (hs : bdd_below s) (ht : bdd_below t) :
bdd_below (s + t)
theorem bdd_below.mul {M : Type u_1} [has_mul M] [preorder M] {s t : set M} (hs : bdd_below s) (ht : bdd_below t) :
bdd_below (s * t)
theorem csupr_add {ι : Type u_1} {G : Type u_2} [add_group G] [nonempty ι] {f : ι → G} (hf : bdd_above (set.range f)) (a : G) :
(⨆ (i : ι), f i) + a = ⨆ (i : ι), f i + a
theorem csupr_mul {ι : Type u_1} {G : Type u_2} [group G] [nonempty ι] {f : ι → G} (hf : bdd_above (set.range f)) (a : G) :
(⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
theorem csupr_div {ι : Type u_1} {G : Type u_2} [group G] [nonempty ι] {f : ι → G} (hf : bdd_above (set.range f)) (a : G) :
(⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a
theorem csupr_sub {ι : Type u_1} {G : Type u_2} [add_group G] [nonempty ι] {f : ι → G} (hf : bdd_above (set.range f)) (a : G) :
(⨆ (i : ι), f i) - a = ⨆ (i : ι), f i - a
theorem add_csupr {ι : Type u_1} {G : Type u_2} [add_group G] [nonempty ι] {f : ι → G} (hf : bdd_above (set.range f)) (a : G) :
(a + ⨆ (i : ι), f i) = ⨆ (i : ι), a + f i
theorem mul_csupr {ι : Type u_1} {G : Type u_2} [group G] [nonempty ι] {f : ι → G} (hf : bdd_above (set.range f)) (a : G) :
(a * ⨆ (i : ι), f i) = ⨆ (i : ι), a * f i