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 the forward direction 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)
theorem
metric.bounded.neg
{E : Type u_1}
[semi_normed_group E]
{s : set E} :
metric.bounded s → metric.bounded (-s)
theorem
metric.bounded.sub
{E : Type u_1}
[semi_normed_group E]
{s t : set E}
(hs : metric.bounded s)
(ht : metric.bounded t) :
metric.bounded (s - t)
theorem
inf_edist_neg
{E : Type u_1}
[semi_normed_group E]
(x : E)
(s : set E) :
emetric.inf_edist (-x) s = emetric.inf_edist x (-s)
@[simp]
theorem
inf_edist_neg_neg
{E : Type u_1}
[semi_normed_group E]
(x : E)
(s : set E) :
emetric.inf_edist (-x) (-s) = emetric.inf_edist x s
@[simp]
theorem
neg_thickening
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(s : set E) :
-metric.thickening δ s = metric.thickening δ (-s)
@[simp]
theorem
neg_cthickening
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(s : set E) :
-metric.cthickening δ s = metric.cthickening δ (-s)
@[simp]
theorem
neg_ball
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x : E) :
-metric.ball x δ = metric.ball (-x) δ
@[simp]
theorem
neg_closed_ball
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x : E) :
-metric.closed_ball x δ = metric.closed_ball (-x) δ
theorem
singleton_add_ball
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x y : E) :
{x} + metric.ball y δ = metric.ball (x + y) δ
theorem
singleton_sub_ball
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x y : E) :
{x} - metric.ball y δ = metric.ball (x - y) δ
theorem
ball_add_singleton
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x y : E) :
metric.ball x δ + {y} = metric.ball (x + y) δ
theorem
ball_sub_singleton
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x y : E) :
metric.ball x δ - {y} = metric.ball (x - y) δ
theorem
singleton_add_ball_zero
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x : E) :
{x} + metric.ball 0 δ = metric.ball x δ
theorem
singleton_sub_ball_zero
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x : E) :
{x} - metric.ball 0 δ = metric.ball x δ
theorem
ball_zero_add_singleton
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x : E) :
metric.ball 0 δ + {x} = metric.ball x δ
theorem
ball_zero_sub_singleton
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x : E) :
metric.ball 0 δ - {x} = metric.ball (-x) δ
theorem
vadd_ball_zero
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x : E) :
x +ᵥ metric.ball 0 δ = metric.ball x δ
@[simp]
theorem
singleton_add_closed_ball
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x y : E) :
{x} + metric.closed_ball y δ = metric.closed_ball (x + y) δ
@[simp]
theorem
singleton_sub_closed_ball
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x y : E) :
{x} - metric.closed_ball y δ = metric.closed_ball (x - y) δ
@[simp]
theorem
closed_ball_add_singleton
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x y : E) :
metric.closed_ball x δ + {y} = metric.closed_ball (x + y) δ
@[simp]
theorem
closed_ball_sub_singleton
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x y : E) :
metric.closed_ball x δ - {y} = metric.closed_ball (x - y) δ
theorem
singleton_add_closed_ball_zero
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x : E) :
{x} + metric.closed_ball 0 δ = metric.closed_ball x δ
theorem
singleton_sub_closed_ball_zero
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x : E) :
{x} - metric.closed_ball 0 δ = metric.closed_ball x δ
theorem
closed_ball_zero_add_singleton
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x : E) :
metric.closed_ball 0 δ + {x} = metric.closed_ball x δ
theorem
closed_ball_zero_sub_singleton
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x : E) :
metric.closed_ball 0 δ - {x} = metric.closed_ball (-x) δ
@[simp]
theorem
vadd_closed_ball_zero
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(x : E) :
x +ᵥ metric.closed_ball 0 δ = metric.closed_ball x δ
theorem
add_ball_zero
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(s : set E) :
s + metric.ball 0 δ = metric.thickening δ s
theorem
sub_ball_zero
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(s : set E) :
s - metric.ball 0 δ = metric.thickening δ s
theorem
ball_add_zero
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(s : set E) :
metric.ball 0 δ + s = metric.thickening δ s
theorem
ball_sub_zero
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(s : set E) :
metric.ball 0 δ - s = metric.thickening δ (-s)
@[simp]
theorem
add_ball
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(s : set E)
(x : E) :
s + metric.ball x δ = x +ᵥ metric.thickening δ s
@[simp]
theorem
sub_ball
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(s : set E)
(x : E) :
s - metric.ball x δ = -x +ᵥ metric.thickening δ s
@[simp]
theorem
ball_add
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(s : set E)
(x : E) :
metric.ball x δ + s = x +ᵥ metric.thickening δ s
@[simp]
theorem
ball_sub
{E : Type u_1}
[semi_normed_group E]
(δ : ℝ)
(s : set E)
(x : E) :
metric.ball x δ - s = x +ᵥ metric.thickening δ (-s)
theorem
is_compact.add_closed_ball_zero
{E : Type u_1}
[semi_normed_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ) :
s + metric.closed_ball 0 δ = metric.cthickening δ s
theorem
is_compact.sub_closed_ball_zero
{E : Type u_1}
[semi_normed_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ) :
s - metric.closed_ball 0 δ = metric.cthickening δ s
theorem
is_compact.closed_ball_zero_add
{E : Type u_1}
[semi_normed_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ) :
metric.closed_ball 0 δ + s = metric.cthickening δ s
theorem
is_compact.closed_ball_zero_sub
{E : Type u_1}
[semi_normed_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ) :
metric.closed_ball 0 δ - s = metric.cthickening δ (-s)
theorem
is_compact.add_closed_ball
{E : Type u_1}
[semi_normed_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ)
(x : E) :
s + metric.closed_ball x δ = x +ᵥ metric.cthickening δ s
theorem
is_compact.sub_closed_ball
{E : Type u_1}
[semi_normed_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ)
(x : E) :
s - metric.closed_ball x δ = -x +ᵥ metric.cthickening δ s
theorem
is_compact.closed_ball_add
{E : Type u_1}
[semi_normed_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ)
(x : E) :
metric.closed_ball x δ + s = x +ᵥ metric.cthickening δ s
theorem
is_compact.closed_ball_sub
{E : Type u_1}
[semi_normed_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ)
(x : E) :
metric.closed_ball x δ + s = x +ᵥ metric.cthickening δ s