Properties of pointwise scalar multiplication of sets in normed spaces. #
We explore the relationships between scalar multiplication of sets in vector spaces, and the norm. Notably, we express arbitrary balls as rescaling of other balls, and we show that the multiplication of bounded sets remain bounded.
theorem
smul_ball
{π : Type u_1}
[normed_field π]
{E : Type u_2}
[semi_normed_group E]
[normed_space π E]
{c : π}
(hc : c β 0)
(x : E)
(r : β) :
c β’ metric.ball x r = metric.ball (c β’ x) (β₯cβ₯ * r)
theorem
smul_sphere'
{π : Type u_1}
[normed_field π]
{E : Type u_2}
[semi_normed_group E]
[normed_space π E]
{c : π}
(hc : c β 0)
(x : E)
(r : β) :
c β’ metric.sphere x r = metric.sphere (c β’ x) (β₯cβ₯ * r)
@[simp]
theorem
normed_space.sphere_nonempty
{E : Type u_1}
[normed_group E]
[normed_space β E]
[nontrivial E]
{x : E}
{r : β} :
(metric.sphere x r).nonempty β 0 β€ r
In a nontrivial real normed space, a sphere is nonempty if and only if its radius is nonnegative.
theorem
smul_sphere
{π : Type u_1}
[normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
[normed_space β E]
[nontrivial E]
(c : π)
(x : E)
{r : β}
(hr : 0 β€ r) :
c β’ metric.sphere x r = metric.sphere (c β’ x) (β₯cβ₯ * r)
theorem
smul_closed_ball'
{π : Type u_1}
[normed_field π]
{E : Type u_2}
[semi_normed_group E]
[normed_space π E]
{c : π}
(hc : c β 0)
(x : E)
(r : β) :
c β’ metric.closed_ball x r = metric.closed_ball (c β’ x) (β₯cβ₯ * r)
theorem
metric.bounded.smul
{π : Type u_1}
[normed_field π]
{E : Type u_2}
[semi_normed_group E]
[normed_space π E]
{s : set E}
(hs : metric.bounded s)
(c : π) :
metric.bounded (c β’ s)
theorem
eventually_singleton_add_smul_subset
{π : Type u_1}
[normed_field π]
{E : Type u_2}
[semi_normed_group E]
[normed_space π E]
{x : E}
{s : set E}
(hs : metric.bounded s)
{u : set E}
(hu : u β π x) :
If s is a bounded set, then for small enough r, the set {x} + r β’ s is contained in any
fixed neighborhood of x.
theorem
set_smul_mem_nhds_zero
{π : Type u_1}
[normed_field π]
{E : Type u_2}
[semi_normed_group E]
[normed_space π E]
{s : set E}
(hs : s β π 0)
{c : π}
(hc : c β 0) :
theorem
set_smul_mem_nhds_zero_iff
{π : Type u_1}
[normed_field π]
{E : Type u_2}
[semi_normed_group E]
[normed_space π E]
(s : set E)
{c : π}
(hc : c β 0) :
theorem
smul_closed_ball
{π : Type u_1}
[normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
(c : π)
(x : E)
{r : β}
(hr : 0 β€ r) :
c β’ metric.closed_ball x r = metric.closed_ball (c β’ x) (β₯cβ₯ * r)