HepLean Documentation

Mathlib.Data.Real.Pointwise

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