mathlib3 documentation

algebra.bounds

Upper/lower bounds in ordered monoids and groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove a few facts like “-s is bounded above iff s is bounded below” (bdd_above_neg).

@[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} (h : is_glb s a) :
is_lub (-s) (-a)
@[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} (h : is_lub s a) :
is_glb (-s) (-a)
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) :
( (i : ι), f i) + a = (i : ι), f i + a
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) :
( (i : ι), f i) * a = (i : ι), f i * a
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) :
( (i : ι), f i) / a = (i : ι), f i / a
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) :
( (i : ι), f i) - a = (i : ι), f i - a
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) :
(a + (i : ι), f i) = (i : ι), a + f i
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) :
(a * (i : ι), f i) = (i : ι), a * f i