mathlib3 documentation

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} [linear_ordered_field α] [mul_action_with_zero α ] [ordered_smul α ] {a : α} (ha : 0 a) (s : set ) :
theorem real.smul_infi_of_nonneg {ι : Sort u_1} {α : Type u_2} [linear_ordered_field α] [mul_action_with_zero α ] [ordered_smul α ] {a : α} (ha : 0 a) (f : ι ) :
(a (i : ι), f i) = (i : ι), a f i
theorem real.Sup_smul_of_nonneg {α : Type u_2} [linear_ordered_field α] [mul_action_with_zero α ] [ordered_smul α ] {a : α} (ha : 0 a) (s : set ) :
theorem real.smul_supr_of_nonneg {ι : Sort u_1} {α : Type u_2} [linear_ordered_field α] [mul_action_with_zero α ] [ordered_smul α ] {a : α} (ha : 0 a) (f : ι ) :
(a (i : ι), f i) = (i : ι), a f i
theorem real.Inf_smul_of_nonpos {α : Type u_2} [linear_ordered_field α] [module α ] [ordered_smul α ] {a : α} (ha : a 0) (s : set ) :
theorem real.smul_supr_of_nonpos {ι : Sort u_1} {α : Type u_2} [linear_ordered_field α] [module α ] [ordered_smul α ] {a : α} (ha : a 0) (f : ι ) :
(a (i : ι), f i) = (i : ι), a f i
theorem real.Sup_smul_of_nonpos {α : Type u_2} [linear_ordered_field α] [module α ] [ordered_smul α ] {a : α} (ha : a 0) (s : set ) :
theorem real.smul_infi_of_nonpos {ι : Sort u_1} {α : Type u_2} [linear_ordered_field α] [module α ] [ordered_smul α ] {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