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