# 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 Bornology.IsBounded.add {E : Type u_1} {s : Set E} {t : Set E} (hs : ) (ht : ) :
theorem Bornology.IsBounded.mul {E : Type u_1} [] {s : Set E} {t : Set E} (hs : ) (ht : ) :
theorem Bornology.IsBounded.of_add {E : Type u_1} {s : Set E} {t : Set E} (hst : Bornology.IsBounded (s + t)) :
theorem Bornology.IsBounded.of_mul {E : Type u_1} [] {s : Set E} {t : Set E} (hst : Bornology.IsBounded (s * t)) :
theorem Bornology.IsBounded.neg {E : Type u_1} {s : Set E} :
theorem Bornology.IsBounded.inv {E : Type u_1} [] {s : Set E} :
theorem Bornology.IsBounded.sub {E : Type u_1} {s : Set E} {t : Set E} (hs : ) (ht : ) :
theorem Bornology.IsBounded.div {E : Type u_1} [] {s : Set E} {t : Set E} (hs : ) (ht : ) :
@[simp]
theorem infEdist_neg_neg {E : Type u_1} (x : E) (s : Set E) :
@[simp]
theorem infEdist_inv_inv {E : Type u_1} (x : E) (s : Set E) :
theorem infEdist_neg {E : Type u_1} (x : E) (s : Set E) :
=
theorem infEdist_inv {E : Type u_1} (x : E) (s : Set E) :
theorem ediam_add_le {E : Type u_1} (x : Set E) (y : Set E) :
theorem ediam_mul_le {E : Type u_1} (x : Set E) (y : Set E) :
@[simp]
theorem neg_thickening {E : Type u_1} (δ : ) (s : Set E) :
=
@[simp]
theorem inv_thickening {E : Type u_1} (δ : ) (s : Set E) :
()⁻¹ =
@[simp]
theorem neg_cthickening {E : Type u_1} (δ : ) (s : Set E) :
=
@[simp]
theorem inv_cthickening {E : Type u_1} (δ : ) (s : Set E) :
@[simp]
theorem neg_ball {E : Type u_1} (δ : ) (x : E) :
@[simp]
theorem inv_ball {E : Type u_1} (δ : ) (x : E) :
()⁻¹ =
@[simp]
theorem neg_closedBall {E : Type u_1} (δ : ) (x : E) :
=
@[simp]
theorem inv_closedBall {E : Type u_1} (δ : ) (x : E) :
()⁻¹ =
theorem singleton_add_ball {E : Type u_1} (δ : ) (x : E) (y : E) :
{x} + = Metric.ball (x + y) δ
theorem singleton_mul_ball {E : Type u_1} (δ : ) (x : E) (y : E) :
{x} * = Metric.ball (x * y) δ
theorem singleton_sub_ball {E : Type u_1} (δ : ) (x : E) (y : E) :
{x} - = Metric.ball (x - y) δ
theorem singleton_div_ball {E : Type u_1} (δ : ) (x : E) (y : E) :
{x} / = Metric.ball (x / y) δ
theorem ball_add_singleton {E : Type u_1} (δ : ) (x : E) (y : E) :
+ {y} = Metric.ball (x + y) δ
theorem ball_mul_singleton {E : Type u_1} (δ : ) (x : E) (y : E) :
* {y} = Metric.ball (x * y) δ
theorem ball_sub_singleton {E : Type u_1} (δ : ) (x : E) (y : E) :
- {y} = Metric.ball (x - y) δ
theorem ball_div_singleton {E : Type u_1} (δ : ) (x : E) (y : E) :
/ {y} = Metric.ball (x / y) δ
theorem singleton_add_ball_zero {E : Type u_1} (δ : ) (x : E) :
{x} + =
theorem singleton_mul_ball_one {E : Type u_1} (δ : ) (x : E) :
{x} * =
theorem singleton_sub_ball_zero {E : Type u_1} (δ : ) (x : E) :
{x} - =
theorem singleton_div_ball_one {E : Type u_1} (δ : ) (x : E) :
{x} / =
theorem ball_zero_add_singleton {E : Type u_1} (δ : ) (x : E) :
+ {x} =
theorem ball_one_mul_singleton {E : Type u_1} (δ : ) (x : E) :
* {x} =
theorem ball_zero_sub_singleton {E : Type u_1} (δ : ) (x : E) :
- {x} = Metric.ball (-x) δ
theorem ball_one_div_singleton {E : Type u_1} (δ : ) (x : E) :
/ {x} =
theorem vadd_ball_zero {E : Type u_1} (δ : ) (x : E) :
x +ᵥ =
theorem smul_ball_one {E : Type u_1} (δ : ) (x : E) :
x =
@[simp]
theorem singleton_add_closedBall {E : Type u_1} (δ : ) (x : E) (y : E) :
{x} + = Metric.closedBall (x + y) δ
@[simp]
theorem singleton_mul_closedBall {E : Type u_1} (δ : ) (x : E) (y : E) :
{x} * = Metric.closedBall (x * y) δ
@[simp]
theorem singleton_sub_closedBall {E : Type u_1} (δ : ) (x : E) (y : E) :
{x} - = Metric.closedBall (x - y) δ
@[simp]
theorem singleton_div_closedBall {E : Type u_1} (δ : ) (x : E) (y : E) :
{x} / = Metric.closedBall (x / y) δ
@[simp]
theorem closedBall_add_singleton {E : Type u_1} (δ : ) (x : E) (y : E) :
+ {y} = Metric.closedBall (x + y) δ
@[simp]
theorem closedBall_mul_singleton {E : Type u_1} (δ : ) (x : E) (y : E) :
* {y} = Metric.closedBall (x * y) δ
@[simp]
theorem closedBall_sub_singleton {E : Type u_1} (δ : ) (x : E) (y : E) :
- {y} = Metric.closedBall (x - y) δ
@[simp]
theorem closedBall_div_singleton {E : Type u_1} (δ : ) (x : E) (y : E) :
/ {y} = Metric.closedBall (x / y) δ
theorem singleton_add_closedBall_zero {E : Type u_1} (δ : ) (x : E) :
{x} + =
theorem singleton_mul_closedBall_one {E : Type u_1} (δ : ) (x : E) :
{x} * =
theorem singleton_sub_closedBall_zero {E : Type u_1} (δ : ) (x : E) :
{x} - =
theorem singleton_div_closedBall_one {E : Type u_1} (δ : ) (x : E) :
{x} / =
theorem closedBall_zero_add_singleton {E : Type u_1} (δ : ) (x : E) :
+ {x} =
theorem closedBall_one_mul_singleton {E : Type u_1} (δ : ) (x : E) :
* {x} =
theorem closedBall_zero_sub_singleton {E : Type u_1} (δ : ) (x : E) :
- {x} =
theorem closedBall_one_div_singleton {E : Type u_1} (δ : ) (x : E) :
/ {x} =
@[simp]
theorem vadd_closedBall_zero {E : Type u_1} (δ : ) (x : E) :
x +ᵥ =
@[simp]
theorem smul_closedBall_one {E : Type u_1} (δ : ) (x : E) :
x =
theorem add_ball_zero {E : Type u_1} (δ : ) (s : Set E) :
s + =
theorem mul_ball_one {E : Type u_1} (δ : ) (s : Set E) :
s * =
theorem sub_ball_zero {E : Type u_1} (δ : ) (s : Set E) :
s - =
theorem div_ball_one {E : Type u_1} (δ : ) (s : Set E) :
s / =
theorem ball_add_zero {E : Type u_1} (δ : ) (s : Set E) :
+ s =
theorem ball_mul_one {E : Type u_1} (δ : ) (s : Set E) :
* s =
theorem ball_sub_zero {E : Type u_1} (δ : ) (s : Set E) :
- s =
theorem ball_div_one {E : Type u_1} (δ : ) (s : Set E) :
/ s =
@[simp]
theorem add_ball {E : Type u_1} (δ : ) (s : Set E) (x : E) :
s + = x +ᵥ
@[simp]
theorem mul_ball {E : Type u_1} (δ : ) (s : Set E) (x : E) :
s * = x
@[simp]
theorem sub_ball {E : Type u_1} (δ : ) (s : Set E) (x : E) :
s - = -x +ᵥ
@[simp]
theorem div_ball {E : Type u_1} (δ : ) (s : Set E) (x : E) :
s / = x⁻¹
@[simp]
theorem ball_add {E : Type u_1} (δ : ) (s : Set E) (x : E) :
+ s = x +ᵥ
@[simp]
theorem ball_mul {E : Type u_1} (δ : ) (s : Set E) (x : E) :
* s = x
@[simp]
theorem ball_sub {E : Type u_1} (δ : ) (s : Set E) (x : E) :
- s = x +ᵥ
@[simp]
theorem ball_div {E : Type u_1} (δ : ) (s : Set E) (x : E) :
/ s = x
theorem IsCompact.add_closedBall_zero {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) :
s + =
theorem IsCompact.mul_closedBall_one {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) :
s * =
theorem IsCompact.sub_closedBall_zero {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) :
s - =
theorem IsCompact.div_closedBall_one {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) :
s / =
theorem IsCompact.closedBall_zero_add {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) :
+ s =
theorem IsCompact.closedBall_one_mul {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) :
* s =
theorem IsCompact.closedBall_zero_sub {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) :
- s =
theorem IsCompact.closedBall_one_div {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) :
/ s =
theorem IsCompact.add_closedBall {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) (x : E) :
s + = x +ᵥ
theorem IsCompact.mul_closedBall {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) (x : E) :
s * = x
theorem IsCompact.sub_closedBall {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) (x : E) :
s - =
theorem IsCompact.div_closedBall {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) (x : E) :
s / =
theorem IsCompact.closedBall_add {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) (x : E) :
+ s = x +ᵥ
theorem IsCompact.closedBall_mul {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) (x : E) :
* s = x
theorem IsCompact.closedBall_sub {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) (x : E) :
+ s = x +ᵥ
theorem IsCompact.closedBall_div {E : Type u_1} {δ : } {s : Set E} (hs : ) (hδ : 0 δ) (x : E) :
* s = x