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 ℝ) :
has_Inf.Inf (a • s) = a • has_Inf.Inf s
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 : ι → ℝ) :
theorem
real.Sup_smul_of_nonneg
{α : Type u_2}
[linear_ordered_field α]
[mul_action_with_zero α ℝ]
[ordered_smul α ℝ]
{a : α}
(ha : 0 ≤ a)
(s : set ℝ) :
has_Sup.Sup (a • s) = a • has_Sup.Sup s
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 : ι → ℝ) :
theorem
real.Inf_smul_of_nonpos
{α : Type u_2}
[linear_ordered_field α]
[module α ℝ]
[ordered_smul α ℝ]
{a : α}
(ha : a ≤ 0)
(s : set ℝ) :
has_Inf.Inf (a • s) = a • has_Sup.Sup s
theorem
real.Sup_smul_of_nonpos
{α : Type u_2}
[linear_ordered_field α]
[module α ℝ]
[ordered_smul α ℝ]
{a : α}
(ha : a ≤ 0)
(s : set ℝ) :
has_Sup.Sup (a • s) = a • has_Inf.Inf s