Documentation

Mathlib.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” (bddAbove_neg).

@[simp]
theorem bddAbove_neg {G : Type u_1} [AddGroup G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] {s : Set G} :
@[simp]
theorem bddAbove_inv {G : Type u_1} [Group G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] {s : Set G} :
@[simp]
theorem bddBelow_neg {G : Type u_1} [AddGroup G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] {s : Set G} :
@[simp]
theorem bddBelow_inv {G : Type u_1} [Group G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] {s : Set G} :
theorem BddAbove.neg {G : Type u_1} [AddGroup G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] {s : Set G} (h : BddAbove s) :
theorem BddAbove.inv {G : Type u_1} [Group G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] {s : Set G} (h : BddAbove s) :
theorem BddBelow.neg {G : Type u_1} [AddGroup G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] {s : Set G} (h : BddBelow s) :
theorem BddBelow.inv {G : Type u_1} [Group G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] {s : Set G} (h : BddBelow s) :
@[simp]
theorem isLUB_neg {G : Type u_1} [AddGroup G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] {s : Set G} {a : G} :
IsLUB (-s) a IsGLB s (-a)
@[simp]
theorem isLUB_inv {G : Type u_1} [Group G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] {s : Set G} {a : G} :
theorem isLUB_neg' {G : Type u_1} [AddGroup G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] {s : Set G} {a : G} :
IsLUB (-s) (-a) IsGLB s a
theorem isLUB_inv' {G : Type u_1} [Group G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] {s : Set G} {a : G} :
theorem IsGLB.neg {G : Type u_1} [AddGroup G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] {s : Set G} {a : G} (h : IsGLB s a) :
IsLUB (-s) (-a)
theorem IsGLB.inv {G : Type u_1} [Group G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] {s : Set G} {a : G} (h : IsGLB s a) :
@[simp]
theorem isGLB_neg {G : Type u_1} [AddGroup G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] {s : Set G} {a : G} :
IsGLB (-s) a IsLUB s (-a)
@[simp]
theorem isGLB_inv {G : Type u_1} [Group G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] {s : Set G} {a : G} :
theorem isGLB_neg' {G : Type u_1} [AddGroup G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] {s : Set G} {a : G} :
IsGLB (-s) (-a) IsLUB s a
theorem isGLB_inv' {G : Type u_1} [Group G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] {s : Set G} {a : G} :
theorem IsLUB.neg {G : Type u_1} [AddGroup G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] {s : Set G} {a : G} (h : IsLUB s a) :
IsGLB (-s) (-a)
theorem IsLUB.inv {G : Type u_1} [Group G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] {s : Set G} {a : G} (h : IsLUB s a) :
theorem BddBelow.range_neg {G : Type u_1} [AddGroup G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] {α : Type u_2} {f : αG} (hf : BddBelow (Set.range f)) :
BddAbove (Set.range fun (x : α) => -f x)
theorem BddBelow.range_inv {G : Type u_1} [Group G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] {α : Type u_2} {f : αG} (hf : BddBelow (Set.range f)) :
BddAbove (Set.range fun (x : α) => (f x)⁻¹)
theorem BddAbove.range_neg {G : Type u_1} [AddGroup G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] {α : Type u_2} {f : αG} (hf : BddAbove (Set.range f)) :
BddBelow (Set.range fun (x : α) => -f x)
theorem BddAbove.range_inv {G : Type u_1} [Group G] [Preorder G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] {α : Type u_2} {f : αG} (hf : BddAbove (Set.range f)) :
BddBelow (Set.range fun (x : α) => (f x)⁻¹)
theorem add_mem_upperBounds_add {M : Type u_1} [Add M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {s : Set M} {t : Set M} {a : M} {b : M} (ha : a upperBounds s) (hb : b upperBounds t) :
a + b upperBounds (s + t)
theorem mul_mem_upperBounds_mul {M : Type u_1} [Mul M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {s : Set M} {t : Set M} {a : M} {b : M} (ha : a upperBounds s) (hb : b upperBounds t) :
a * b upperBounds (s * t)
theorem subset_upperBounds_add {M : Type u_1} [Add M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] (s : Set M) (t : Set M) :
theorem subset_upperBounds_mul {M : Type u_1} [Mul M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] (s : Set M) (t : Set M) :
theorem add_mem_lowerBounds_add {M : Type u_1} [Add M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {s : Set M} {t : Set M} {a : M} {b : M} (ha : a lowerBounds s) (hb : b lowerBounds t) :
a + b lowerBounds (s + t)
theorem mul_mem_lowerBounds_mul {M : Type u_1} [Mul M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {s : Set M} {t : Set M} {a : M} {b : M} (ha : a lowerBounds s) (hb : b lowerBounds t) :
a * b lowerBounds (s * t)
theorem subset_lowerBounds_add {M : Type u_1} [Add M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] (s : Set M) (t : Set M) :
theorem subset_lowerBounds_mul {M : Type u_1} [Mul M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] (s : Set M) (t : Set M) :
theorem BddAbove.add {M : Type u_1} [Add M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {s : Set M} {t : Set M} (hs : BddAbove s) (ht : BddAbove t) :
BddAbove (s + t)
theorem BddAbove.mul {M : Type u_1} [Mul M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {s : Set M} {t : Set M} (hs : BddAbove s) (ht : BddAbove t) :
BddAbove (s * t)
theorem BddBelow.add {M : Type u_1} [Add M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {s : Set M} {t : Set M} (hs : BddBelow s) (ht : BddBelow t) :
BddBelow (s + t)
theorem BddBelow.mul {M : Type u_1} [Mul M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {s : Set M} {t : Set M} (hs : BddBelow s) (ht : BddBelow t) :
BddBelow (s * t)
theorem BddAbove.range_add {M : Type u_1} [Add M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {α : Type u_2} {f : αM} {g : αM} (hf : BddAbove (Set.range f)) (hg : BddAbove (Set.range g)) :
BddAbove (Set.range fun (x : α) => f x + g x)
theorem BddAbove.range_mul {M : Type u_1} [Mul M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {α : Type u_2} {f : αM} {g : αM} (hf : BddAbove (Set.range f)) (hg : BddAbove (Set.range g)) :
BddAbove (Set.range fun (x : α) => f x * g x)
theorem BddBelow.range_add {M : Type u_1} [Add M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {α : Type u_2} {f : αM} {g : αM} (hf : BddBelow (Set.range f)) (hg : BddBelow (Set.range g)) :
BddBelow (Set.range fun (x : α) => f x + g x)
theorem BddBelow.range_mul {M : Type u_1} [Mul M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {α : Type u_2} {f : αM} {g : αM} (hf : BddBelow (Set.range f)) (hg : BddBelow (Set.range g)) :
BddBelow (Set.range fun (x : α) => f x * g x)
theorem ciSup_add {ι : Type u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [Nonempty ι] {f : ιG} (hf : BddAbove (Set.range f)) (a : G) :
(⨆ (i : ι), f i) + a = ⨆ (i : ι), f i + a
theorem ciSup_mul {ι : Type u_1} {G : Type u_2} [Group G] [ConditionallyCompleteLattice G] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [Nonempty ι] {f : ιG} (hf : BddAbove (Set.range f)) (a : G) :
(⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
theorem ciSup_sub {ι : Type u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [Nonempty ι] {f : ιG} (hf : BddAbove (Set.range f)) (a : G) :
(⨆ (i : ι), f i) - a = ⨆ (i : ι), f i - a
theorem ciSup_div {ι : Type u_1} {G : Type u_2} [Group G] [ConditionallyCompleteLattice G] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [Nonempty ι] {f : ιG} (hf : BddAbove (Set.range f)) (a : G) :
(⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a
theorem ciInf_add {ι : Type u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [Nonempty ι] {f : ιG} (hf : BddBelow (Set.range f)) (a : G) :
(⨅ (i : ι), f i) + a = ⨅ (i : ι), f i + a
theorem ciInf_mul {ι : Type u_1} {G : Type u_2} [Group G] [ConditionallyCompleteLattice G] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [Nonempty ι] {f : ιG} (hf : BddBelow (Set.range f)) (a : G) :
(⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a
theorem ciInf_sub {ι : Type u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [Nonempty ι] {f : ιG} (hf : BddBelow (Set.range f)) (a : G) :
(⨅ (i : ι), f i) - a = ⨅ (i : ι), f i - a
theorem ciInf_div {ι : Type u_1} {G : Type u_2} [Group G] [ConditionallyCompleteLattice G] [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [Nonempty ι] {f : ιG} (hf : BddBelow (Set.range f)) (a : G) :
(⨅ (i : ι), f i) / a = ⨅ (i : ι), f i / a
theorem add_ciSup {ι : Sort u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [Nonempty ι] {f : ιG} (hf : BddAbove (Set.range f)) (a : G) :
a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
theorem mul_ciSup {ι : Sort u_1} {G : Type u_2} [Group G] [ConditionallyCompleteLattice G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [Nonempty ι] {f : ιG} (hf : BddAbove (Set.range f)) (a : G) :
a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
theorem add_ciInf {ι : Sort u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] [Nonempty ι] {f : ιG} (hf : BddBelow (Set.range f)) (a : G) :
a + ⨅ (i : ι), f i = ⨅ (i : ι), a + f i
theorem mul_ciInf {ι : Sort u_1} {G : Type u_2} [Group G] [ConditionallyCompleteLattice G] [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] [Nonempty ι] {f : ιG} (hf : BddBelow (Set.range f)) (a : G) :
a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i