Pointwise operations on sets of reals

This file relates sInf (a • s)/sSup (a • s) with a • sInf s/a • sSup s for s : Set ℝ.

From these, it relates ⨅ i, a • f i / ⨆ i, a • f i with a • (⨅ i, f i) / a • (⨆ i, f i), and provides lemmas about distributing * over ⨅ and ⨆.

TODO

This is true more generally for conditionally complete linear order whose default value is 0. We don't have those yet.

theorem Real.sInf_smul_of_nonneg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [MulActionWithZero α ℝ] [IsOrderedModule α ℝ] {a : α} (ha : 0 ≤ a) (s : Set ℝ) : sInf (a • s) = a • sInf s

theorem Real.smul_iInf_of_nonneg {ι : Sort u_1} {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [MulActionWithZero α ℝ] [IsOrderedModule α ℝ] {a : α} (ha : 0 ≤ a) (f : ι → ℝ) : a • ⨅ (i : ι), f i = ⨅ (i : ι), a • f i

theorem Real.sSup_smul_of_nonneg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [MulActionWithZero α ℝ] [IsOrderedModule α ℝ] {a : α} (ha : 0 ≤ a) (s : Set ℝ) : sSup (a • s) = a • sSup s

theorem Real.smul_iSup_of_nonneg {ι : Sort u_1} {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [MulActionWithZero α ℝ] [IsOrderedModule α ℝ] {a : α} (ha : 0 ≤ a) (f : ι → ℝ) : a • ⨆ (i : ι), f i = ⨆ (i : ι), a • f i

theorem Real.sInf_smul_of_nonpos {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Module α ℝ] [IsOrderedModule α ℝ] {a : α} (ha : a ≤ 0) (s : Set ℝ) : sInf (a • s) = a • sSup s

theorem Real.smul_iSup_of_nonpos {ι : Sort u_1} {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Module α ℝ] [IsOrderedModule α ℝ] {a : α} (ha : a ≤ 0) (f : ι → ℝ) : a • ⨆ (i : ι), f i = ⨅ (i : ι), a • f i

theorem Real.sSup_smul_of_nonpos {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Module α ℝ] [IsOrderedModule α ℝ] {a : α} (ha : a ≤ 0) (s : Set ℝ) : sSup (a • s) = a • sInf s

theorem Real.smul_iInf_of_nonpos {ι : Sort u_1} {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Module α ℝ] [IsOrderedModule α ℝ] {a : α} (ha : a ≤ 0) (f : ι → ℝ) : a • ⨅ (i : ι), f i = ⨆ (i : ι), a • f i

Special cases for real multiplication

theorem Real.mul_iInf_of_nonneg {ι : Sort u_1} {r : ℝ} (ha : 0 ≤ r) (f : ι → ℝ) : r * ⨅ (i : ι), f i = ⨅ (i : ι), r * f i

theorem Real.mul_iSup_of_nonneg {ι : Sort u_1} {r : ℝ} (ha : 0 ≤ r) (f : ι → ℝ) : r * ⨆ (i : ι), f i = ⨆ (i : ι), r * f i

theorem Real.mul_iInf_of_nonpos {ι : Sort u_1} {r : ℝ} (ha : r ≤ 0) (f : ι → ℝ) : r * ⨅ (i : ι), f i = ⨆ (i : ι), r * f i

theorem Real.mul_iSup_of_nonpos {ι : Sort u_1} {r : ℝ} (ha : r ≤ 0) (f : ι → ℝ) : r * ⨆ (i : ι), f i = ⨅ (i : ι), r * f i

theorem Real.iInf_mul_of_nonneg {ι : Sort u_1} {r : ℝ} (ha : 0 ≤ r) (f : ι → ℝ) : (⨅ (i : ι), f i) * r = ⨅ (i : ι), f i * r

theorem Real.iSup_mul_of_nonneg {ι : Sort u_1} {r : ℝ} (ha : 0 ≤ r) (f : ι → ℝ) : (⨆ (i : ι), f i) * r = ⨆ (i : ι), f i * r

theorem Real.iInf_mul_of_nonpos {ι : Sort u_1} {r : ℝ} (ha : r ≤ 0) (f : ι → ℝ) : (⨅ (i : ι), f i) * r = ⨆ (i : ι), f i * r

theorem Real.iSup_mul_of_nonpos {ι : Sort u_1} {r : ℝ} (ha : r ≤ 0) (f : ι → ℝ) : (⨆ (i : ι), f i) * r = ⨅ (i : ι), f i * r