# mathlibdocumentation

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