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} :

BddAbove (-s) ↔ BddBelow s

source

ink

@[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} :

BddAbove s⁻¹ ↔ BddBelow s

source

ink

@[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} :

BddBelow (-s) ↔ BddAbove s

source

ink

@[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} :

BddBelow s⁻¹ ↔ BddAbove s

source

ink

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

BddBelow (-s)

source

ink

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

BddBelow s⁻¹

source

ink

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

BddAbove (-s)

source

ink

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

BddAbove s⁻¹

source

ink

@[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} :

IsLUB (-s) a ↔ IsGLB s (-a)

source

ink

@[simp]

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} :

IsLUB s⁻¹ a ↔ IsGLB s a⁻¹

source

ink

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} :

IsLUB (-s) (-a) ↔ IsGLB s a

source

ink

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} :

IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a

source

ink

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} (h : IsGLB s a) :

IsLUB (-s) (-a)

source

ink

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} (h : IsGLB s a) :

IsLUB s⁻¹ a⁻¹

source

ink

@[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} :

IsGLB (-s) a ↔ IsLUB s (-a)

source

ink

@[simp]

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} :

IsGLB s⁻¹ a ↔ IsLUB s a⁻¹

source

ink

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} :

IsGLB (-s) (-a) ↔ IsLUB s a

source

ink

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} :

IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a

source

ink

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} (h : IsLUB s a) :

IsGLB (-s) (-a)

source

ink

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} (h : IsLUB s a) :

IsGLB s⁻¹ a⁻¹

source

ink

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)

source

ink

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)

source

ink

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)

source

ink

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)

source

ink

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)

source

ink

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)

source

ink

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)

source

ink

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)

source

ink

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

BddAbove (s + t)

source

ink

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

BddAbove (s * t)

source

ink

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

BddBelow (s + t)

source

ink

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

BddBelow (s * t)

source

ink

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

(⨆ i, f i) + a = ⨆ i, f i + a

source

ink

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

(⨆ i, f i) * a = ⨆ i, f i * a

source

ink

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

(⨆ i, f i) - a = ⨆ i, f i - a

source

ink

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

(⨆ i, f i) / a = ⨆ i, f i / a

source

ink

theorem add_csupᵢ {ι : Type u_2} {G : Type u_1} [inst : AddGroup G] [inst : ConditionallyCompleteLattice G] [inst : CovariantClass G G (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) :

(a + ⨆ i, f i) = ⨆ i, a + f i

source

ink

theorem mul_csupᵢ {ι : Type u_2} {G : Type u_1} [inst : Group G] [inst : ConditionallyCompleteLattice G] [inst : CovariantClass G G (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) :

(a * ⨆ i, f i) = ⨆ i, a * f i