Properties of pointwise addition of sets in normed groups. #
We explore the relationships between pointwise addition of sets in normed groups, and the norm. Notably, we show that the sum of bounded sets remain bounded.
Alias of bounded_iff_exists_norm_le.
theorem
metric.bounded.exists_pos_norm_le
{E : Type u_1}
[semi_normed_group E]
{s : set E}
(hs : metric.bounded s) :
theorem
metric.bounded.add
{E : Type u_1}
[semi_normed_group E]
{s t : set E}
(hs : metric.bounded s)
(ht : metric.bounded t) :
metric.bounded (s + t)
@[simp]
theorem
singleton_add_ball
{E : Type u_1}
[semi_normed_group E]
(x y : E)
(r : ℝ) :
{x} + metric.ball y r = metric.ball (x + y) r
@[simp]
theorem
ball_add_singleton
{E : Type u_1}
[semi_normed_group E]
(x y : E)
(r : ℝ) :
metric.ball x r + {y} = metric.ball (x + y) r
theorem
singleton_add_ball_zero
{E : Type u_1}
[semi_normed_group E]
(x : E)
(r : ℝ) :
{x} + metric.ball 0 r = metric.ball x r
theorem
ball_zero_add_singleton
{E : Type u_1}
[semi_normed_group E]
(x : E)
(r : ℝ) :
metric.ball 0 r + {x} = metric.ball x r
@[simp]
theorem
singleton_add_closed_ball
{E : Type u_1}
[semi_normed_group E]
(x y : E)
(r : ℝ) :
{x} + metric.closed_ball y r = metric.closed_ball (x + y) r
@[simp]
theorem
closed_ball_add_singleton
{E : Type u_1}
[semi_normed_group E]
(x y : E)
(r : ℝ) :
metric.closed_ball x r + {y} = metric.closed_ball (x + y) r
theorem
singleton_add_closed_ball_zero
{E : Type u_1}
[semi_normed_group E]
(x : E)
(r : ℝ) :
{x} + metric.closed_ball 0 r = metric.closed_ball x r
theorem
closed_ball_zero_add_singleton
{E : Type u_1}
[semi_normed_group E]
(x : E)
(r : ℝ) :
metric.closed_ball 0 r + {x} = metric.closed_ball x r
theorem
is_compact.cthickening_eq_add_closed_ball
{E : Type u_1}
[semi_normed_group E]
{s : set E}
(hs : is_compact s)
{r : ℝ}
(hr : 0 ≤ r) :
metric.cthickening r s = s + metric.closed_ball 0 r