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}
[inst : AddGroup G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{s : Set G}
:
@[simp]
theorem
bddAbove_inv
{G : Type u_1}
[inst : Group G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{s : Set G}
:
@[simp]
theorem
bddBelow_neg
{G : Type u_1}
[inst : AddGroup G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{s : Set G}
:
@[simp]
theorem
bddBelow_inv
{G : Type u_1}
[inst : Group G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{s : Set G}
:
theorem
BddAbove.neg
{G : Type u_1}
[inst : AddGroup G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{s : Set G}
(h : BddAbove s)
:
theorem
BddAbove.inv
{G : Type u_1}
[inst : Group G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{s : Set G}
(h : BddAbove s)
:
theorem
BddBelow.neg
{G : Type u_1}
[inst : AddGroup G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{s : Set G}
(h : BddBelow s)
:
theorem
BddBelow.inv
{G : Type u_1}
[inst : Group G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{s : Set G}
(h : BddBelow s)
:
@[simp]
theorem
isLUB_neg'
{G : Type u_1}
[inst : AddGroup G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{s : Set G}
{a : G}
:
theorem
isLUB_inv'
{G : Type u_1}
[inst : Group G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{s : Set G}
{a : G}
:
@[simp]
theorem
isGLB_neg'
{G : Type u_1}
[inst : AddGroup G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{s : Set G}
{a : G}
:
theorem
isGLB_inv'
{G : Type u_1}
[inst : Group G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{s : Set G}
{a : G}
:
theorem
add_mem_upperBounds_add
{M : Type u_1}
[inst : Add M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{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}
[inst : Mul M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{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}
[inst : Add M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(s : Set M)
(t : Set M)
:
upperBounds s + upperBounds t ⊆ upperBounds (s + t)
theorem
subset_upperBounds_mul
{M : Type u_1}
[inst : Mul M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(s : Set M)
(t : Set M)
:
upperBounds s * upperBounds t ⊆ upperBounds (s * t)
theorem
add_mem_lowerBounds_add
{M : Type u_1}
[inst : Add M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{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}
[inst : Mul M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{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}
[inst : Add M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(s : Set M)
(t : Set M)
:
lowerBounds s + lowerBounds t ⊆ lowerBounds (s + t)
theorem
subset_lowerBounds_mul
{M : Type u_1}
[inst : Mul M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(s : Set M)
(t : Set M)
:
lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t)
theorem
BddAbove.add
{M : Type u_1}
[inst : Add M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{s : Set M}
{t : Set M}
(hs : BddAbove s)
(ht : BddAbove t)
:
theorem
BddAbove.mul
{M : Type u_1}
[inst : Mul M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{s : Set M}
{t : Set M}
(hs : BddAbove s)
(ht : BddAbove t)
:
theorem
BddBelow.add
{M : Type u_1}
[inst : Add M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{s : Set M}
{t : Set M}
(hs : BddBelow s)
(ht : BddBelow t)
:
theorem
BddBelow.mul
{M : Type u_1}
[inst : Mul M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{s : Set M}
{t : Set M}
(hs : BddBelow s)
(ht : BddBelow t)
:
theorem
csupᵢ_add
{ι : Type u_2}
{G : Type u_1}
[inst : AddGroup G]
[inst : ConditionallyCompleteLattice G]
[inst : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : Nonempty ι]
{f : ι → G}
(hf : BddAbove (Set.range f))
(a : G)
:
theorem
csupᵢ_mul
{ι : Type u_2}
{G : Type u_1}
[inst : Group G]
[inst : ConditionallyCompleteLattice G]
[inst : CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : Nonempty ι]
{f : ι → G}
(hf : BddAbove (Set.range f))
(a : G)
:
theorem
csupᵢ_sub
{ι : Type u_2}
{G : Type u_1}
[inst : AddGroup G]
[inst : ConditionallyCompleteLattice G]
[inst : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : Nonempty ι]
{f : ι → G}
(hf : BddAbove (Set.range f))
(a : G)
:
theorem
csupᵢ_div
{ι : Type u_2}
{G : Type u_1}
[inst : Group G]
[inst : ConditionallyCompleteLattice G]
[inst : CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : Nonempty ι]
{f : ι → G}
(hf : BddAbove (Set.range f))
(a : G)
: