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
add_mem_upperBounds_add
{M : Type u_3}
[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_3}
[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_3}
[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)
:
upperBounds s + upperBounds t ⊆ upperBounds (s + t)
theorem
subset_upperBounds_mul
{M : Type u_3}
[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)
:
upperBounds s * upperBounds t ⊆ upperBounds (s * t)
theorem
add_mem_lowerBounds_add
{M : Type u_3}
[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_3}
[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_3}
[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)
:
lowerBounds s + lowerBounds t ⊆ lowerBounds (s + t)
theorem
subset_lowerBounds_mul
{M : Type u_3}
[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)
:
lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t)
theorem
BddAbove.add
{M : Type u_3}
[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)
:
theorem
BddAbove.mul
{M : Type u_3}
[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)
:
theorem
BddBelow.add
{M : Type u_3}
[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)
:
theorem
BddBelow.mul
{M : Type u_3}
[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)
:
theorem
BddAbove.range_add
{ι : Type u_1}
{M : Type u_3}
[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]
{f : ι → M}
{g : ι → M}
(hf : BddAbove (Set.range f))
(hg : BddAbove (Set.range g))
:
theorem
BddAbove.range_mul
{ι : Type u_1}
{M : Type u_3}
[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]
{f : ι → M}
{g : ι → M}
(hf : BddAbove (Set.range f))
(hg : BddAbove (Set.range g))
:
theorem
BddBelow.range_add
{ι : Type u_1}
{M : Type u_3}
[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]
{f : ι → M}
{g : ι → M}
(hf : BddBelow (Set.range f))
(hg : BddBelow (Set.range g))
:
theorem
BddBelow.range_mul
{ι : Type u_1}
{M : Type u_3}
[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]
{f : ι → M}
{g : ι → M}
(hf : BddBelow (Set.range f))
(hg : BddBelow (Set.range g))
:
@[simp]
theorem
bddAbove_neg
{G : Type u_2}
[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_2}
[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_2}
[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_2}
[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_2}
[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_2}
[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_2}
[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_2}
[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)
:
theorem
isLUB_neg'
{G : Type u_2}
[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}
:
theorem
isLUB_inv'
{G : Type u_2}
[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_2}
[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}
:
theorem
isGLB_inv'
{G : Type u_2}
[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
BddBelow.range_neg
{G : Type u_2}
[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_4}
{f : α → G}
(hf : BddBelow (Set.range f))
:
theorem
BddBelow.range_inv
{G : Type u_2}
[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_4}
{f : α → G}
(hf : BddBelow (Set.range f))
:
theorem
BddAbove.range_neg
{G : Type u_2}
[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_4}
{f : α → G}
(hf : BddAbove (Set.range f))
:
theorem
BddAbove.range_inv
{G : Type u_2}
[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_4}
{f : α → G}
(hf : BddAbove (Set.range f))
: