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.
theorem
metric.bounded.add
{E : Type u_1}
[seminormed_add_group E]
{s t : set E}
(hs : metric.bounded s)
(ht : metric.bounded t) :
metric.bounded (s + t)
theorem
metric.bounded.mul
{E : Type u_1}
[seminormed_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}
[seminormed_add_group E]
{s : set E} :
metric.bounded s → metric.bounded (-s)
theorem
metric.bounded.div
{E : Type u_1}
[seminormed_group E]
{s t : set E}
(hs : metric.bounded s)
(ht : metric.bounded t) :
metric.bounded (s / t)
theorem
metric.bounded.sub
{E : Type u_1}
[seminormed_add_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}
[seminormed_add_comm_group E]
(x : E)
(s : set E) :
emetric.inf_edist (-x) s = emetric.inf_edist x (-s)
theorem
inf_edist_inv
{E : Type u_1}
[seminormed_comm_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}
[seminormed_add_comm_group E]
(x : E)
(s : set E) :
emetric.inf_edist (-x) (-s) = emetric.inf_edist x s
@[simp]
theorem
inf_edist_inv_inv
{E : Type u_1}
[seminormed_comm_group E]
(x : E)
(s : set E) :
emetric.inf_edist x⁻¹ s⁻¹ = emetric.inf_edist x s
@[simp]
theorem
inv_thickening
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(s : set E) :
(metric.thickening δ s)⁻¹ = metric.thickening δ s⁻¹
@[simp]
theorem
neg_thickening
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(s : set E) :
-metric.thickening δ s = metric.thickening δ (-s)
@[simp]
theorem
inv_cthickening
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(s : set E) :
(metric.cthickening δ s)⁻¹ = metric.cthickening δ s⁻¹
@[simp]
theorem
neg_cthickening
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(s : set E) :
-metric.cthickening δ s = metric.cthickening δ (-s)
@[simp]
theorem
neg_ball
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x : E) :
-metric.ball x δ = metric.ball (-x) δ
@[simp]
theorem
inv_ball
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x : E) :
(metric.ball x δ)⁻¹ = metric.ball x⁻¹ δ
@[simp]
theorem
neg_closed_ball
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x : E) :
-metric.closed_ball x δ = metric.closed_ball (-x) δ
@[simp]
theorem
inv_closed_ball
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x : E) :
(metric.closed_ball x δ)⁻¹ = metric.closed_ball x⁻¹ δ
theorem
singleton_add_ball
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x y : E) :
{x} + metric.ball y δ = metric.ball (x + y) δ
theorem
singleton_mul_ball
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x y : E) :
{x} * metric.ball y δ = metric.ball (x * y) δ
theorem
singleton_sub_ball
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x y : E) :
{x} - metric.ball y δ = metric.ball (x - y) δ
theorem
singleton_div_ball
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x y : E) :
{x} / metric.ball y δ = metric.ball (x / y) δ
theorem
ball_mul_singleton
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x y : E) :
metric.ball x δ * {y} = metric.ball (x * y) δ
theorem
ball_add_singleton
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x y : E) :
metric.ball x δ + {y} = metric.ball (x + y) δ
theorem
ball_div_singleton
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x y : E) :
metric.ball x δ / {y} = metric.ball (x / y) δ
theorem
ball_sub_singleton
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x y : E) :
metric.ball x δ - {y} = metric.ball (x - y) δ
theorem
singleton_add_ball_zero
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x : E) :
{x} + metric.ball 0 δ = metric.ball x δ
theorem
singleton_mul_ball_one
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x : E) :
{x} * metric.ball 1 δ = metric.ball x δ
theorem
singleton_div_ball_one
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x : E) :
{x} / metric.ball 1 δ = metric.ball x δ
theorem
singleton_sub_ball_zero
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x : E) :
{x} - metric.ball 0 δ = metric.ball x δ
theorem
ball_zero_add_singleton
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x : E) :
metric.ball 0 δ + {x} = metric.ball x δ
theorem
ball_one_mul_singleton
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x : E) :
metric.ball 1 δ * {x} = metric.ball x δ
theorem
ball_one_div_singleton
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x : E) :
metric.ball 1 δ / {x} = metric.ball x⁻¹ δ
theorem
ball_zero_sub_singleton
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x : E) :
metric.ball 0 δ - {x} = metric.ball (-x) δ
theorem
vadd_ball_zero
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x : E) :
x +ᵥ metric.ball 0 δ = metric.ball x δ
theorem
smul_ball_one
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x : E) :
x • metric.ball 1 δ = metric.ball x δ
@[simp]
theorem
singleton_mul_closed_ball
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x y : E) :
{x} * metric.closed_ball y δ = metric.closed_ball (x * y) δ
@[simp]
theorem
singleton_add_closed_ball
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x y : E) :
{x} + metric.closed_ball y δ = metric.closed_ball (x + y) δ
@[simp]
theorem
singleton_div_closed_ball
{E : Type u_1}
[seminormed_comm_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}
[seminormed_add_comm_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}
[seminormed_add_comm_group E]
(δ : ℝ)
(x y : E) :
metric.closed_ball x δ + {y} = metric.closed_ball (x + y) δ
@[simp]
theorem
closed_ball_mul_singleton
{E : Type u_1}
[seminormed_comm_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}
[seminormed_add_comm_group E]
(δ : ℝ)
(x y : E) :
metric.closed_ball x δ - {y} = metric.closed_ball (x - y) δ
@[simp]
theorem
closed_ball_div_singleton
{E : Type u_1}
[seminormed_comm_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}
[seminormed_add_comm_group E]
(δ : ℝ)
(x : E) :
{x} + metric.closed_ball 0 δ = metric.closed_ball x δ
theorem
singleton_mul_closed_ball_one
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x : E) :
{x} * metric.closed_ball 1 δ = metric.closed_ball x δ
theorem
singleton_div_closed_ball_one
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x : E) :
{x} / metric.closed_ball 1 δ = metric.closed_ball x δ
theorem
singleton_sub_closed_ball_zero
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x : E) :
{x} - metric.closed_ball 0 δ = metric.closed_ball x δ
theorem
closed_ball_one_mul_singleton
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x : E) :
metric.closed_ball 1 δ * {x} = metric.closed_ball x δ
theorem
closed_ball_zero_add_singleton
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x : E) :
metric.closed_ball 0 δ + {x} = metric.closed_ball x δ
theorem
closed_ball_one_div_singleton
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x : E) :
metric.closed_ball 1 δ / {x} = metric.closed_ball x⁻¹ δ
theorem
closed_ball_zero_sub_singleton
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x : E) :
metric.closed_ball 0 δ - {x} = metric.closed_ball (-x) δ
@[simp]
theorem
vadd_closed_ball_zero
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(x : E) :
x +ᵥ metric.closed_ball 0 δ = metric.closed_ball x δ
@[simp]
theorem
smul_closed_ball_one
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(x : E) :
x • metric.closed_ball 1 δ = metric.closed_ball x δ
theorem
mul_ball_one
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(s : set E) :
s * metric.ball 1 δ = metric.thickening δ s
theorem
add_ball_zero
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(s : set E) :
s + metric.ball 0 δ = metric.thickening δ s
theorem
sub_ball_zero
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(s : set E) :
s - metric.ball 0 δ = metric.thickening δ s
theorem
div_ball_one
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(s : set E) :
s / metric.ball 1 δ = metric.thickening δ s
theorem
ball_add_zero
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(s : set E) :
metric.ball 0 δ + s = metric.thickening δ s
theorem
ball_mul_one
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(s : set E) :
metric.ball 1 δ * s = metric.thickening δ s
theorem
ball_div_one
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(s : set E) :
metric.ball 1 δ / s = metric.thickening δ s⁻¹
theorem
ball_sub_zero
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(s : set E) :
metric.ball 0 δ - s = metric.thickening δ (-s)
@[simp]
theorem
add_ball
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(s : set E)
(x : E) :
s + metric.ball x δ = x +ᵥ metric.thickening δ s
@[simp]
theorem
mul_ball
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(s : set E)
(x : E) :
s * metric.ball x δ = x • metric.thickening δ s
@[simp]
theorem
sub_ball
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(s : set E)
(x : E) :
s - metric.ball x δ = -x +ᵥ metric.thickening δ s
@[simp]
theorem
div_ball
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(s : set E)
(x : E) :
s / metric.ball x δ = x⁻¹ • metric.thickening δ s
@[simp]
theorem
ball_mul
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(s : set E)
(x : E) :
metric.ball x δ * s = x • metric.thickening δ s
@[simp]
theorem
ball_add
{E : Type u_1}
[seminormed_add_comm_group E]
(δ : ℝ)
(s : set E)
(x : E) :
metric.ball x δ + s = x +ᵥ metric.thickening δ s
@[simp]
theorem
ball_div
{E : Type u_1}
[seminormed_comm_group E]
(δ : ℝ)
(s : set E)
(x : E) :
metric.ball x δ / s = x • metric.thickening δ s⁻¹
@[simp]
theorem
ball_sub
{E : Type u_1}
[seminormed_add_comm_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}
[seminormed_add_comm_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ) :
s + metric.closed_ball 0 δ = metric.cthickening δ s
theorem
is_compact.mul_closed_ball_one
{E : Type u_1}
[seminormed_comm_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ) :
s * metric.closed_ball 1 δ = metric.cthickening δ s
theorem
is_compact.sub_closed_ball_zero
{E : Type u_1}
[seminormed_add_comm_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ) :
s - metric.closed_ball 0 δ = metric.cthickening δ s
theorem
is_compact.div_closed_ball_one
{E : Type u_1}
[seminormed_comm_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ) :
s / metric.closed_ball 1 δ = metric.cthickening δ s
theorem
is_compact.closed_ball_one_mul
{E : Type u_1}
[seminormed_comm_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ) :
metric.closed_ball 1 δ * s = metric.cthickening δ s
theorem
is_compact.closed_ball_zero_add
{E : Type u_1}
[seminormed_add_comm_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}
[seminormed_add_comm_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ) :
metric.closed_ball 0 δ - s = metric.cthickening δ (-s)
theorem
is_compact.closed_ball_one_div
{E : Type u_1}
[seminormed_comm_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ) :
metric.closed_ball 1 δ / s = metric.cthickening δ s⁻¹
theorem
is_compact.mul_closed_ball
{E : Type u_1}
[seminormed_comm_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.add_closed_ball
{E : Type u_1}
[seminormed_add_comm_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}
[seminormed_add_comm_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.div_closed_ball
{E : Type u_1}
[seminormed_comm_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}
[seminormed_add_comm_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_mul
{E : Type u_1}
[seminormed_comm_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_div
{E : Type u_1}
[seminormed_comm_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}
[seminormed_add_comm_group E]
{δ : ℝ}
{s : set E}
(hs : is_compact s)
(hδ : 0 ≤ δ)
(x : E) :
metric.closed_ball x δ + s = x +ᵥ metric.cthickening δ s