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.

theorem Real.sInf_smul_of_nonneg {α : Type u_2} [LinearOrderedField α] [MulActionWithZero α ] [OrderedSMul α ] {a : α} (ha : 0 a) (s : Set ) :
sInf (a s) = a sInf s
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
theorem Real.sSup_smul_of_nonneg {α : Type u_2} [LinearOrderedField α] [MulActionWithZero α ] [OrderedSMul α ] {a : α} (ha : 0 a) (s : Set ) :
sSup (a s) = a sSup s
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
theorem Real.sInf_smul_of_nonpos {α : Type u_2} [LinearOrderedField α] [Module α ] [OrderedSMul α ] {a : α} (ha : a 0) (s : Set ) :
sInf (a s) = a sSup s
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
theorem Real.sSup_smul_of_nonpos {α : Type u_2} [LinearOrderedField α] [Module α ] [OrderedSMul α ] {a : α} (ha : a 0) (s : Set ) :
sSup (a s) = a sInf s
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 #

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