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 ℝ
.
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.smul_supr_of_nonpos
{ι : Sort u_1}
{α : Type u_2}
[linear_ordered_field α]
[module α ℝ]
[ordered_smul α ℝ]
{a : α}
(ha : a ≤ 0)
(f : ι → ℝ) :
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
theorem
real.smul_infi_of_nonpos
{ι : Sort u_1}
{α : Type u_2}
[linear_ordered_field α]
[module α ℝ]
[ordered_smul α ℝ]
{a : α}
(ha : a ≤ 0)
(f : ι → ℝ) :