Properties of pointwise addition of sets in normed groups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.of_add
{E : Type u_1}
[seminormed_add_group E]
{s t : set E}
(hst : metric.bounded (s + t)) :
theorem
metric.bounded.of_mul
{E : Type u_1}
[seminormed_group E]
{s t : set E}
(hst : 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
theorem
ediam_add_le
{E : Type u_1}
[seminormed_add_comm_group E]
(x y : set E) :
emetric.diam (x + y) ≤ emetric.diam x + emetric.diam y
theorem
ediam_mul_le
{E : Type u_1}
[seminormed_comm_group E]
(x y : set E) :
emetric.diam (x * y) ≤ emetric.diam x + emetric.diam y
@[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