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} [LinearOrderedField α] [MulActionWithZero α ℝ] [OrderedSMul α ℝ] {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} [LinearOrderedField α] [MulActionWithZero α ℝ] [OrderedSMul α ℝ] {a : α} (ha : 0 ≤ a) (f : ι → ℝ) :

a • ⨅ i, f i = ⨅ i, a • f i

source

theorem Real.sSup_smul_of_nonneg {α : Type u_2} [LinearOrderedField α] [MulActionWithZero α ℝ] [OrderedSMul α ℝ] {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} [LinearOrderedField α] [MulActionWithZero α ℝ] [OrderedSMul α ℝ] {a : α} (ha : 0 ≤ a) (f : ι → ℝ) :

a • ⨆ i, f i = ⨆ i, a • f i

source

theorem Real.sInf_smul_of_nonpos {α : Type u_2} [LinearOrderedField α] [Module α ℝ] [OrderedSMul α ℝ] {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} [LinearOrderedField α] [Module α ℝ] [OrderedSMul α ℝ] {a : α} (ha : a ≤ 0) (f : ι → ℝ) :

a • ⨆ i, f i = ⨅ i, a • f i

source

theorem Real.sSup_smul_of_nonpos {α : Type u_2} [LinearOrderedField α] [Module α ℝ] [OrderedSMul α ℝ] {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} [LinearOrderedField α] [Module α ℝ] [OrderedSMul α ℝ] {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