# 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} [] [Zero α] :
sSup 0 = 0
@[simp]
theorem sSup_one {α : Type u_1} [] [One α] :
sSup 1 = 1
@[simp]
theorem sInf_zero {α : Type u_1} [] [Zero α] :
sInf 0 = 0
@[simp]
theorem sInf_one {α : Type u_1} [] [One α] :
sInf 1 = 1
theorem sSup_neg {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (s : Set α) :
sSup (-s) = -sInf s
theorem sSup_inv {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (s : Set α) :
theorem sInf_neg {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (s : Set α) :
sInf (-s) = -sSup s
theorem sInf_inv {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (s : Set α) :
theorem sSup_add {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (s : Set α) (t : Set α) :
sSup (s + t) = sSup s + sSup t
theorem sSup_mul {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (s : Set α) (t : Set α) :
sSup (s * t) = sSup s * sSup t
theorem sInf_add {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (s : Set α) (t : Set α) :
sInf (s + t) = sInf s + sInf t
theorem sInf_mul {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (s : Set α) (t : Set α) :
sInf (s * t) = sInf s * sInf t
theorem sSup_sub {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (s : Set α) (t : Set α) :
sSup (s - t) = sSup s - sInf t
theorem sSup_div {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (s : Set α) (t : Set α) :
sSup (s / t) = sSup s / sInf t
theorem sInf_sub {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (s : Set α) (t : Set α) :
sInf (s - t) = sInf s - sSup t
theorem sInf_div {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (s : Set α) (t : Set α) :
sInf (s / t) = sInf s / sSup t
@[simp]
theorem csSup_zero {α : Type u_1} [Zero α] :
sSup 0 = 0
@[simp]
theorem csSup_one {α : Type u_1} [One α] :
sSup 1 = 1
@[simp]
theorem csInf_zero {α : Type u_1} [Zero α] :
sInf 0 = 0
@[simp]
theorem csInf_one {α : Type u_1} [One α] :
sInf 1 = 1
theorem csSup_neg {α : Type u_1} [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {s : Set α} (hs₀ : s.Nonempty) (hs₁ : ) :
sSup (-s) = -sInf s
theorem csSup_inv {α : Type u_1} [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {s : Set α} (hs₀ : s.Nonempty) (hs₁ : ) :
theorem csInf_neg {α : Type u_1} [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {s : Set α} (hs₀ : s.Nonempty) (hs₁ : ) :
sInf (-s) = -sSup s
theorem csInf_inv {α : Type u_1} [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {s : Set α} (hs₀ : s.Nonempty) (hs₁ : ) :
theorem csSup_add {α : Type u_1} [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : ) (ht₀ : t.Nonempty) (ht₁ : ) :
sSup (s + t) = sSup s + sSup t
theorem csSup_mul {α : Type u_1} [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : ) (ht₀ : t.Nonempty) (ht₁ : ) :
sSup (s * t) = sSup s * sSup t
theorem csInf_add {α : Type u_1} [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : ) (ht₀ : t.Nonempty) (ht₁ : ) :
sInf (s + t) = sInf s + sInf t
theorem csInf_mul {α : Type u_1} [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : ) (ht₀ : t.Nonempty) (ht₁ : ) :
sInf (s * t) = sInf s * sInf t
theorem csSup_sub {α : Type u_1} [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : ) (ht₀ : t.Nonempty) (ht₁ : ) :
sSup (s - t) = sSup s - sInf t
theorem csSup_div {α : Type u_1} [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : ) (ht₀ : t.Nonempty) (ht₁ : ) :
sSup (s / t) = sSup s / sInf t
theorem csInf_sub {α : Type u_1} [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : ) (ht₀ : t.Nonempty) (ht₁ : ) :
sInf (s - t) = sInf s - sSup t
theorem csInf_div {α : Type u_1} [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {s : Set α} {t : Set α} (hs₀ : s.Nonempty) (hs₁ : ) (ht₀ : t.Nonempty) (ht₁ : ) :
sInf (s / t) = sInf s / sSup t
theorem LinearOrderedField.smul_Ioo {K : Type u_2} {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} {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} {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} {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} {a : K} {r : K} (hr : 0 < r) :
r = Set.Ioi (r a)
theorem LinearOrderedField.smul_Iio {K : Type u_2} {a : K} {r : K} (hr : 0 < r) :
r = Set.Iio (r a)
theorem LinearOrderedField.smul_Ici {K : Type u_2} {a : K} {r : K} (hr : 0 < r) :
r = Set.Ici (r a)
theorem LinearOrderedField.smul_Iic {K : Type u_2} {a : K} {r : K} (hr : 0 < r) :
r = Set.Iic (r a)