# 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.

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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 #

source
theorem Real.mul_iInf_of_nonneg {ι : Sort u_1} {r : ℝ} (ha : 0 ≤ r) (f : ι → ℝ) :
r * ⨅ (i : ι), f i = ⨅ (i : ι), r * f i
source
theorem Real.mul_iSup_of_nonneg {ι : Sort u_1} {r : ℝ} (ha : 0 ≤ r) (f : ι → ℝ) :
r * ⨆ (i : ι), f i = ⨆ (i : ι), r * f i
source
theorem Real.mul_iInf_of_nonpos {ι : Sort u_1} {r : ℝ} (ha : r ≤ 0) (f : ι → ℝ) :
r * ⨅ (i : ι), f i = ⨆ (i : ι), r * f i
source
theorem Real.mul_iSup_of_nonpos {ι : Sort u_1} {r : ℝ} (ha : r ≤ 0) (f : ι → ℝ) :
r * ⨆ (i : ι), f i = ⨅ (i : ι), r * f i
source
theorem Real.iInf_mul_of_nonneg {ι : Sort u_1} {r : ℝ} (ha : 0 ≤ r) (f : ι → ℝ) :
(⨅ (i : ι), f i) * r = ⨅ (i : ι), f i * r
source
theorem Real.iSup_mul_of_nonneg {ι : Sort u_1} {r : ℝ} (ha : 0 ≤ r) (f : ι → ℝ) :
(⨆ (i : ι), f i) * r = ⨆ (i : ι), f i * r
source
theorem Real.iInf_mul_of_nonpos {ι : Sort u_1} {r : ℝ} (ha : r ≤ 0) (f : ι → ℝ) :
(⨅ (i : ι), f i) * r = ⨆ (i : ι), f i * r
source
theorem Real.iSup_mul_of_nonpos {ι : Sort u_1} {r : ℝ} (ha : r ≤ 0) (f : ι → ℝ) :
(⨆ (i : ι), f i) * r = ⨅ (i : ι), f i * r