mathlib documentation

data.real.pointwise

Pointwise operations on sets of reals #

This file relates Inf (a • s)/Sup (a • s) with a • Inf s/a • Sup s for s : set.

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_1} [linear_ordered_field α] [mul_action_with_zero α ] [ordered_smul α ] {a : α} (ha : 0 a) (s : set ) :
Inf (a s) = a Inf s
theorem real.Sup_smul_of_nonneg {α : Type u_1} [linear_ordered_field α] [mul_action_with_zero α ] [ordered_smul α ] {a : α} (ha : 0 a) (s : set ) :
Sup (a s) = a Sup s
theorem real.Inf_smul_of_nonpos {α : Type u_1} [linear_ordered_field α] [module α ] [ordered_smul α ] {a : α} (ha : a 0) (s : set ) :
Inf (a s) = a Sup s
theorem real.Sup_smul_of_nonpos {α : Type u_1} [linear_ordered_field α] [module α ] [ordered_smul α ] {a : α} (ha : a 0) (s : set ) :
Sup (a s) = a Inf s