Pointwise operations on ordered algebraic objects

This file contains lemmas about the effect of pointwise operations on sets with an order structure.

TODO

sSup (s • t) = sSup s • sSup t and sInf (s • t) = sInf s • sInf t hold as well but CovariantClass is currently not polymorphic enough to state it.

@[simp]

theorem sSup_zero {α : Type u_1} [CompleteLattice α] [Zero α] : sSup 0 = 0

@[simp]

theorem sSup_one {α : Type u_1} [CompleteLattice α] [One α] : sSup 1 = 1

@[simp]

theorem sInf_zero {α : Type u_1} [CompleteLattice α] [Zero α] : sInf 0 = 0

@[simp]

theorem sInf_one {α : Type u_1} [CompleteLattice α] [One α] : sInf 1 = 1

theorem sSup_neg {α : Type u_1} [CompleteLattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (s : Set α) : sSup (-s) = -sInf s

theorem sSup_inv {α : Type u_1} [CompleteLattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (s : Set α) : sSup s⁻¹ = (sInf s)⁻¹

theorem sInf_neg {α : Type u_1} [CompleteLattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (s : Set α) : sInf (-s) = -sSup s

theorem sInf_inv {α : Type u_1} [CompleteLattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (s : Set α) : sInf s⁻¹ = (sSup s)⁻¹

theorem sSup_add {α : Type u_1} [CompleteLattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (s : Set α) (t : Set α) : sSup (s + t) = sSup s + sSup t

theorem sSup_mul {α : Type u_1} [CompleteLattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (s : Set α) (t : Set α) : sSup (s * t) = sSup s * sSup t

theorem sInf_add {α : Type u_1} [CompleteLattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (s : Set α) (t : Set α) : sInf (s + t) = sInf s + sInf t

theorem sInf_mul {α : Type u_1} [CompleteLattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (s : Set α) (t : Set α) : sInf (s * t) = sInf s * sInf t

theorem sSup_sub {α : Type u_1} [CompleteLattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (s : Set α) (t : Set α) : sSup (s - t) = sSup s - sInf t

theorem sSup_div {α : Type u_1} [CompleteLattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (s : Set α) (t : Set α) : sSup (s / t) = sSup s / sInf t

theorem sInf_sub {α : Type u_1} [CompleteLattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (s : Set α) (t : Set α) : sInf (s - t) = sInf s - sSup t

theorem sInf_div {α : Type u_1} [CompleteLattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (s : Set α) (t : Set α) : sInf (s / t) = sInf s / sSup t

@[simp]

theorem csSup_zero {α : Type u_1} [ConditionallyCompleteLattice α] [Zero α] : sSup 0 = 0

@[simp]

theorem csSup_one {α : Type u_1} [ConditionallyCompleteLattice α] [One α] : sSup 1 = 1

@[simp]

theorem csInf_zero {α : Type u_1} [ConditionallyCompleteLattice α] [Zero α] : sInf 0 = 0

@[simp]

theorem csInf_one {α : Type u_1} [ConditionallyCompleteLattice α] [One α] : sInf 1 = 1

theorem csSup_neg {α : Type u_1} [ConditionallyCompleteLattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} (hs₀ : s.Nonempty) (hs₁ : BddBelow s) : sSup (-s) = -sInf s

theorem csSup_inv {α : Type u_1} [ConditionallyCompleteLattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} (hs₀ : s.Nonempty) (hs₁ : BddBelow s) : sSup s⁻¹ = (sInf s)⁻¹

theorem csInf_neg {α : Type u_1} [ConditionallyCompleteLattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} (hs₀ : s.Nonempty) (hs₁ : BddAbove s) : sInf (-s) = -sSup s

theorem csInf_inv {α : Type u_1} [ConditionallyCompleteLattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} (hs₀ : s.Nonempty) (hs₁ : BddAbove s) : sInf s⁻¹ = (sSup s)⁻¹

theorem csSup_add {α : Type u_1} [ConditionallyCompleteLattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : sSup (s + t) = sSup s + sSup t

theorem csSup_mul {α : Type u_1} [ConditionallyCompleteLattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : sSup (s * t) = sSup s * sSup t

theorem csInf_add {α : Type u_1} [ConditionallyCompleteLattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) : sInf (s + t) = sInf s + sInf t

theorem csInf_mul {α : Type u_1} [ConditionallyCompleteLattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) : sInf (s * t) = sInf s * sInf t

theorem csSup_sub {α : Type u_1} [ConditionallyCompleteLattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) : sSup (s - t) = sSup s - sInf t

theorem csSup_div {α : Type u_1} [ConditionallyCompleteLattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) : sSup (s / t) = sSup s / sInf t

theorem csInf_sub {α : Type u_1} [ConditionallyCompleteLattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : sInf (s - t) = sInf s - sSup t

theorem csInf_div {α : Type u_1} [ConditionallyCompleteLattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : sInf (s / t) = sInf s / sSup t

theorem LinearOrderedField.smul_Ioo {K : Type u_2} [LinearOrderedField K] {a : K} {b : K} {r : K} (hr : 0 < r) : r • Set.Ioo a b = Set.Ioo (r • a) (r • b)

theorem LinearOrderedField.smul_Icc {K : Type u_2} [LinearOrderedField K] {a : K} {b : K} {r : K} (hr : 0 < r) : r • Set.Icc a b = Set.Icc (r • a) (r • b)

theorem LinearOrderedField.smul_Ico {K : Type u_2} [LinearOrderedField K] {a : K} {b : K} {r : K} (hr : 0 < r) : r • Set.Ico a b = Set.Ico (r • a) (r • b)

theorem LinearOrderedField.smul_Ioc {K : Type u_2} [LinearOrderedField K] {a : K} {b : K} {r : K} (hr : 0 < r) : r • Set.Ioc a b = Set.Ioc (r • a) (r • b)

theorem LinearOrderedField.smul_Ioi {K : Type u_2} [LinearOrderedField K] {a : K} {r : K} (hr : 0 < r) : r • Set.Ioi a = Set.Ioi (r • a)

theorem LinearOrderedField.smul_Iio {K : Type u_2} [LinearOrderedField K] {a : K} {r : K} (hr : 0 < r) : r • Set.Iio a = Set.Iio (r • a)

theorem LinearOrderedField.smul_Ici {K : Type u_2} [LinearOrderedField K] {a : K} {r : K} (hr : 0 < r) : r • Set.Ici a = Set.Ici (r • a)

theorem LinearOrderedField.smul_Iic {K : Type u_2} [LinearOrderedField K] {a : K} {r : K} (hr : 0 < r) : r • Set.Iic a = Set.Iic (r • a)