# mathlib3documentation

data.real.pointwise

# Pointwise operations on sets of reals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file relates Inf (a • s)/Sup (a • s) with a • Inf s/a • Sup 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.Inf_smul_of_nonneg {α : Type u_2} [ ] {a : α} (ha : 0 a) (s : set ) :
has_Inf.Inf (a s) = a
theorem real.smul_infi_of_nonneg {ι : Sort u_1} {α : Type u_2} [ ] {a : α} (ha : 0 a) (f : ι ) :
(a (i : ι), f i) = (i : ι), a f i
theorem real.Sup_smul_of_nonneg {α : Type u_2} [ ] {a : α} (ha : 0 a) (s : set ) :
has_Sup.Sup (a s) = a
theorem real.smul_supr_of_nonneg {ι : Sort u_1} {α : Type u_2} [ ] {a : α} (ha : 0 a) (f : ι ) :
(a (i : ι), f i) = (i : ι), a f i
theorem real.Inf_smul_of_nonpos {α : Type u_2} [ ] [ ] {a : α} (ha : a 0) (s : set ) :
has_Inf.Inf (a s) = a
theorem real.smul_supr_of_nonpos {ι : Sort u_1} {α : Type u_2} [ ] [ ] {a : α} (ha : a 0) (f : ι ) :
(a (i : ι), f i) = (i : ι), a f i
theorem real.Sup_smul_of_nonpos {α : Type u_2} [ ] [ ] {a : α} (ha : a 0) (s : set ) :
has_Sup.Sup (a s) = a
theorem real.smul_infi_of_nonpos {ι : Sort u_1} {α : Type u_2} [ ] [ ] {a : α} (ha : a 0) (f : ι ) :
(a (i : ι), f i) = (i : ι), a f i

## Special cases for real multiplication #

theorem real.mul_infi_of_nonneg {ι : Sort u_1} {r : } (ha : 0 r) (f : ι ) :
(r * (i : ι), f i) = (i : ι), r * f i
theorem real.mul_supr_of_nonneg {ι : Sort u_1} {r : } (ha : 0 r) (f : ι ) :
(r * (i : ι), f i) = (i : ι), r * f i
theorem real.mul_infi_of_nonpos {ι : Sort u_1} {r : } (ha : r 0) (f : ι ) :
(r * (i : ι), f i) = (i : ι), r * f i
theorem real.mul_supr_of_nonpos {ι : Sort u_1} {r : } (ha : r 0) (f : ι ) :
(r * (i : ι), f i) = (i : ι), r * f i
theorem real.infi_mul_of_nonneg {ι : Sort u_1} {r : } (ha : 0 r) (f : ι ) :
( (i : ι), f i) * r = (i : ι), f i * r
theorem real.supr_mul_of_nonneg {ι : Sort u_1} {r : } (ha : 0 r) (f : ι ) :
( (i : ι), f i) * r = (i : ι), f i * r
theorem real.infi_mul_of_nonpos {ι : Sort u_1} {r : } (ha : r 0) (f : ι ) :
( (i : ι), f i) * r = (i : ι), f i * r
theorem real.supr_mul_of_nonpos {ι : Sort u_1} {r : } (ha : r 0) (f : ι ) :
( (i : ι), f i) * r = (i : ι), f i * r