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

theorem mul_mem_upperBounds_mul {M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] {s t : Set M} {a b : M} (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : a * b ∈ upperBounds (s * t)

theorem add_mem_upperBounds_add {M : Type u_3} [Add M] [Preorder M] [AddLeftMono M] [AddRightMono M] {s t : Set M} {a b : M} (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : a + b ∈ upperBounds (s + t)

theorem subset_upperBounds_mul {M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] (s t : Set M) : upperBounds s * upperBounds t ⊆ upperBounds (s * t)

theorem subset_upperBounds_add {M : Type u_3} [Add M] [Preorder M] [AddLeftMono M] [AddRightMono M] (s t : Set M) : upperBounds s + upperBounds t ⊆ upperBounds (s + t)

theorem mul_mem_lowerBounds_mul {M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] {s t : Set M} {a b : M} (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : a * b ∈ lowerBounds (s * t)

theorem add_mem_lowerBounds_add {M : Type u_3} [Add M] [Preorder M] [AddLeftMono M] [AddRightMono M] {s t : Set M} {a b : M} (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : a + b ∈ lowerBounds (s + t)

theorem subset_lowerBounds_mul {M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] (s t : Set M) : lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t)

theorem subset_lowerBounds_add {M : Type u_3} [Add M] [Preorder M] [AddLeftMono M] [AddRightMono M] (s t : Set M) : lowerBounds s + lowerBounds t ⊆ lowerBounds (s + t)

theorem BddAbove.mul {M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] {s t : Set M} (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t)

theorem BddAbove.add {M : Type u_3} [Add M] [Preorder M] [AddLeftMono M] [AddRightMono M] {s t : Set M} (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s + t)

theorem BddBelow.mul {M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] {s t : Set M} (hs : BddBelow s) (ht : BddBelow t) : BddBelow (s * t)

theorem BddBelow.add {M : Type u_3} [Add M] [Preorder M] [AddLeftMono M] [AddRightMono M] {s t : Set M} (hs : BddBelow s) (ht : BddBelow t) : BddBelow (s + t)

theorem Set.BddAbove.mul {M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] {s t : Set M} (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t)

Alias of BddAbove.mul.

theorem Set.BddAbove.add {M : Type u_3} [Add M] [Preorder M] [AddLeftMono M] [AddRightMono M] {s t : Set M} (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s + t)

Alias of BddAbove.add.

theorem BddAbove.range_mul {ι : Type u_1} {M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] {f g : ι → M} (hf : BddAbove (Set.range f)) (hg : BddAbove (Set.range g)) : BddAbove (Set.range fun (i : ι) => f i * g i)

theorem BddAbove.range_add {ι : Type u_1} {M : Type u_3} [Add M] [Preorder M] [AddLeftMono M] [AddRightMono M] {f g : ι → M} (hf : BddAbove (Set.range f)) (hg : BddAbove (Set.range g)) : BddAbove (Set.range fun (i : ι) => f i + g i)

theorem BddBelow.range_mul {ι : Type u_1} {M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] {f g : ι → M} (hf : BddBelow (Set.range f)) (hg : BddBelow (Set.range g)) : BddBelow (Set.range fun (i : ι) => f i * g i)

theorem BddBelow.range_add {ι : Type u_1} {M : Type u_3} [Add M] [Preorder M] [AddLeftMono M] [AddRightMono M] {f g : ι → M} (hf : BddBelow (Set.range f)) (hg : BddBelow (Set.range g)) : BddBelow (Set.range fun (i : ι) => f i + g i)

@[simp]

theorem bddAbove_inv {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} : BddAbove s⁻¹ ↔ BddBelow s

@[simp]

theorem bddAbove_neg {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} : BddAbove (-s) ↔ BddBelow s

@[simp]

theorem bddBelow_inv {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} : BddBelow s⁻¹ ↔ BddAbove s

@[simp]

theorem bddBelow_neg {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} : BddBelow (-s) ↔ BddAbove s

theorem BddAbove.inv {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} (h : BddAbove s) : BddBelow s⁻¹

theorem BddAbove.neg {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} (h : BddAbove s) : BddBelow (-s)

theorem BddBelow.inv {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} (h : BddBelow s) : BddAbove s⁻¹

theorem BddBelow.neg {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} (h : BddBelow s) : BddAbove (-s)

@[simp]

theorem isLUB_inv {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G} : IsLUB s⁻¹ a ↔ IsGLB s a⁻¹

@[simp]

theorem isLUB_neg {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G} : IsLUB (-s) a ↔ IsGLB s (-a)

theorem isLUB_inv' {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G} : IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a

theorem isLUB_neg' {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G} : IsLUB (-s) (-a) ↔ IsGLB s a

theorem IsGLB.inv {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G} (h : IsGLB s a) : IsLUB s⁻¹ a⁻¹

theorem IsGLB.neg {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G} (h : IsGLB s a) : IsLUB (-s) (-a)

@[simp]

theorem isGLB_inv {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G} : IsGLB s⁻¹ a ↔ IsLUB s a⁻¹

@[simp]

theorem isGLB_neg {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G} : IsGLB (-s) a ↔ IsLUB s (-a)

theorem isGLB_inv' {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G} : IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a

theorem isGLB_neg' {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G} : IsGLB (-s) (-a) ↔ IsLUB s a

theorem IsLUB.inv {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G} (h : IsLUB s a) : IsGLB s⁻¹ a⁻¹

theorem IsLUB.neg {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G} (h : IsLUB s a) : IsGLB (-s) (-a)

theorem BddBelow.range_inv {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {α : Type u_4} {f : α → G} (hf : BddBelow (Set.range f)) : BddAbove (Set.range fun (x : α) => (f x)⁻¹)

theorem BddBelow.range_neg {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {α : Type u_4} {f : α → G} (hf : BddBelow (Set.range f)) : BddAbove (Set.range fun (x : α) => -f x)

theorem BddAbove.range_inv {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {α : Type u_4} {f : α → G} (hf : BddAbove (Set.range f)) : BddBelow (Set.range fun (x : α) => (f x)⁻¹)

theorem BddAbove.range_neg {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {α : Type u_4} {f : α → G} (hf : BddAbove (Set.range f)) : BddBelow (Set.range fun (x : α) => -f x)

theorem IsLUB.mul {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s t : Set G} {a b : G} (hs : IsLUB s a) (ht : IsLUB t b) : IsLUB (s * t) (a * b)

theorem IsLUB.add {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s t : Set G} {a b : G} (hs : IsLUB s a) (ht : IsLUB t b) : IsLUB (s + t) (a + b)

theorem IsGLB.mul {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s t : Set G} {a b : G} (hs : IsGLB s a) (ht : IsGLB t b) : IsGLB (s * t) (a * b)

theorem IsGLB.add {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s t : Set G} {a b : G} (hs : IsGLB s a) (ht : IsGLB t b) : IsGLB (s + t) (a + b)

theorem IsLUB.div {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s t : Set G} {a b : G} (hs : IsLUB s a) (ht : IsGLB t b) : IsLUB (s / t) (a / b)

theorem IsLUB.sub {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s t : Set G} {a b : G} (hs : IsLUB s a) (ht : IsGLB t b) : IsLUB (s - t) (a - b)

theorem IsGLB.div {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s t : Set G} {a b : G} (hs : IsGLB s a) (ht : IsLUB t b) : IsGLB (s / t) (a / b)

theorem IsGLB.sub {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s t : Set G} {a b : G} (hs : IsGLB s a) (ht : IsLUB t b) : IsGLB (s - t) (a - b)