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).

source
@[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} :
bdd_above (-s) ↔ bdd_below s
source
@[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} :
bdd_above s⁻¹ ↔ bdd_below s
source
@[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} :
bdd_below (-s) ↔ bdd_above s
source
@[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} :
bdd_below s⁻¹ ↔ bdd_above s
source
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) :
bdd_below (-s)
source
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) :
bdd_below s⁻¹
source
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) :
bdd_above s⁻¹
source
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) :
bdd_above (-s)
source
@[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} :
is_lub (-s) a ↔ is_glb s (-a)
source
@[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} :
is_lub s⁻¹ a ↔ is_glb s a⁻¹
source
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} :
is_lub (-s) (-a) ↔ is_glb s a
source
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} :
is_lub s⁻¹ a⁻¹ ↔ is_glb s a
source
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) :
is_lub s⁻¹ a⁻¹
source
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)
source
@[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} :
is_glb (-s) a ↔ is_lub s (-a)
source
@[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} :
is_glb s⁻¹ a ↔ is_lub s a⁻¹
source
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} :
is_glb (-s) (-a) ↔ is_lub s a
source
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} :
is_glb s⁻¹ a⁻¹ ↔ is_lub s a
source
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) :
is_glb s⁻¹ a⁻¹
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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) :
bdd_above (s + t)
source
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) :
bdd_above (s * t)
source
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) :
bdd_below (s + t)
source
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) :
bdd_below (s * t)
source
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
source
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
source
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
source
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
source
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
source
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