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.mul {E : Type u_1} [SeminormedGroup E] {s t : Set E} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) : Bornology.IsBounded (s * t)

theorem Bornology.IsBounded.add {E : Type u_1} [SeminormedAddGroup E] {s t : Set E} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) : Bornology.IsBounded (s + t)

theorem Bornology.IsBounded.of_mul {E : Type u_1} [SeminormedGroup E] {s t : Set E} (hst : Bornology.IsBounded (s * t)) : Bornology.IsBounded s ∨ Bornology.IsBounded t

theorem Bornology.IsBounded.of_add {E : Type u_1} [SeminormedAddGroup E] {s t : Set E} (hst : Bornology.IsBounded (s + t)) : Bornology.IsBounded s ∨ Bornology.IsBounded t

theorem Bornology.IsBounded.inv {E : Type u_1} [SeminormedGroup E] {s : Set E} : Bornology.IsBounded s → Bornology.IsBounded s⁻¹

theorem Bornology.IsBounded.neg {E : Type u_1} [SeminormedAddGroup E] {s : Set E} : Bornology.IsBounded s → Bornology.IsBounded (-s)

theorem Bornology.IsBounded.div {E : Type u_1} [SeminormedGroup E] {s t : Set E} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) : Bornology.IsBounded (s / t)

theorem Bornology.IsBounded.sub {E : Type u_1} [SeminormedAddGroup E] {s t : Set E} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) : Bornology.IsBounded (s - t)

@[simp]

theorem infEdist_inv_inv {E : Type u_1} [SeminormedCommGroup E] (x : E) (s : Set E) : EMetric.infEdist x⁻¹ s⁻¹ = EMetric.infEdist x s

@[simp]

theorem infEdist_neg_neg {E : Type u_1} [SeminormedAddCommGroup E] (x : E) (s : Set E) : EMetric.infEdist (-x) (-s) = EMetric.infEdist x s

theorem infEdist_inv {E : Type u_1} [SeminormedCommGroup E] (x : E) (s : Set E) : EMetric.infEdist x⁻¹ s = EMetric.infEdist x s⁻¹

theorem infEdist_neg {E : Type u_1} [SeminormedAddCommGroup E] (x : E) (s : Set E) : EMetric.infEdist (-x) s = EMetric.infEdist x (-s)

theorem ediam_mul_le {E : Type u_1} [SeminormedCommGroup E] (x y : Set E) : EMetric.diam (x * y) ≤ EMetric.diam x + EMetric.diam y

theorem ediam_add_le {E : Type u_1} [SeminormedAddCommGroup E] (x y : Set E) : EMetric.diam (x + y) ≤ EMetric.diam x + EMetric.diam y

@[simp]

theorem inv_thickening {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) : (Metric.thickening δ s)⁻¹ = Metric.thickening δ s⁻¹

@[simp]

theorem neg_thickening {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) : -Metric.thickening δ s = Metric.thickening δ (-s)

@[simp]

theorem inv_cthickening {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) : (Metric.cthickening δ s)⁻¹ = Metric.cthickening δ s⁻¹

@[simp]

theorem neg_cthickening {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) : -Metric.cthickening δ s = Metric.cthickening δ (-s)

@[simp]

theorem inv_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : (Metric.ball x δ)⁻¹ = Metric.ball x⁻¹ δ

@[simp]

theorem neg_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : -Metric.ball x δ = Metric.ball (-x) δ

@[simp]

theorem inv_closedBall {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : (Metric.closedBall x δ)⁻¹ = Metric.closedBall x⁻¹ δ

@[simp]

theorem neg_closedBall {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : -Metric.closedBall x δ = Metric.closedBall (-x) δ

theorem singleton_mul_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : {x} * Metric.ball y δ = Metric.ball (x * y) δ

theorem singleton_add_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : {x} + Metric.ball y δ = Metric.ball (x + y) δ

theorem singleton_div_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : {x} / Metric.ball y δ = Metric.ball (x / y) δ

theorem singleton_sub_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : {x} - Metric.ball y δ = Metric.ball (x - y) δ

theorem ball_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : Metric.ball x δ * {y} = Metric.ball (x * y) δ

theorem ball_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : Metric.ball x δ + {y} = Metric.ball (x + y) δ

theorem ball_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : Metric.ball x δ / {y} = Metric.ball (x / y) δ

theorem ball_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : Metric.ball x δ - {y} = Metric.ball (x - y) δ

theorem singleton_mul_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : {x} * Metric.ball 1 δ = Metric.ball x δ

theorem singleton_add_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : {x} + Metric.ball 0 δ = Metric.ball x δ

theorem singleton_div_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : {x} / Metric.ball 1 δ = Metric.ball x δ

theorem singleton_sub_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : {x} - Metric.ball 0 δ = Metric.ball x δ

theorem ball_one_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : Metric.ball 1 δ * {x} = Metric.ball x δ

theorem ball_zero_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : Metric.ball 0 δ + {x} = Metric.ball x δ

theorem ball_one_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : Metric.ball 1 δ / {x} = Metric.ball x⁻¹ δ

theorem ball_zero_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : Metric.ball 0 δ - {x} = Metric.ball (-x) δ

theorem smul_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : x • Metric.ball 1 δ = Metric.ball x δ

theorem vadd_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : x +ᵥ Metric.ball 0 δ = Metric.ball x δ

@[simp]

theorem singleton_mul_closedBall {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : {x} * Metric.closedBall y δ = Metric.closedBall (x * y) δ

@[simp]

theorem singleton_add_closedBall {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : {x} + Metric.closedBall y δ = Metric.closedBall (x + y) δ

@[simp]

theorem singleton_div_closedBall {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : {x} / Metric.closedBall y δ = Metric.closedBall (x / y) δ

@[simp]

theorem singleton_sub_closedBall {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : {x} - Metric.closedBall y δ = Metric.closedBall (x - y) δ

@[simp]

theorem closedBall_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : Metric.closedBall x δ * {y} = Metric.closedBall (x * y) δ

@[simp]

theorem closedBall_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : Metric.closedBall x δ + {y} = Metric.closedBall (x + y) δ

@[simp]

theorem closedBall_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : Metric.closedBall x δ / {y} = Metric.closedBall (x / y) δ

@[simp]

theorem closedBall_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : Metric.closedBall x δ - {y} = Metric.closedBall (x - y) δ

theorem singleton_mul_closedBall_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : {x} * Metric.closedBall 1 δ = Metric.closedBall x δ

theorem singleton_add_closedBall_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : {x} + Metric.closedBall 0 δ = Metric.closedBall x δ

theorem singleton_div_closedBall_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : {x} / Metric.closedBall 1 δ = Metric.closedBall x δ

theorem singleton_sub_closedBall_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : {x} - Metric.closedBall 0 δ = Metric.closedBall x δ

theorem closedBall_one_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : Metric.closedBall 1 δ * {x} = Metric.closedBall x δ

theorem closedBall_zero_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : Metric.closedBall 0 δ + {x} = Metric.closedBall x δ

theorem closedBall_one_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : Metric.closedBall 1 δ / {x} = Metric.closedBall x⁻¹ δ

theorem closedBall_zero_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : Metric.closedBall 0 δ - {x} = Metric.closedBall (-x) δ

@[simp]

theorem smul_closedBall_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : x • Metric.closedBall 1 δ = Metric.closedBall x δ

@[simp]

theorem vadd_closedBall_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : x +ᵥ Metric.closedBall 0 δ = Metric.closedBall x δ

theorem mul_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) : s * Metric.ball 1 δ = Metric.thickening δ s

theorem add_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) : s + Metric.ball 0 δ = Metric.thickening δ s

theorem div_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) : s / Metric.ball 1 δ = Metric.thickening δ s

theorem sub_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) : s - Metric.ball 0 δ = Metric.thickening δ s

theorem ball_mul_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) : Metric.ball 1 δ * s = Metric.thickening δ s

theorem ball_add_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) : Metric.ball 0 δ + s = Metric.thickening δ s

theorem ball_div_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) : Metric.ball 1 δ / s = Metric.thickening δ s⁻¹

theorem ball_sub_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) : Metric.ball 0 δ - s = Metric.thickening δ (-s)

@[simp]

theorem mul_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E) : s * Metric.ball x δ = x • Metric.thickening δ s

@[simp]

theorem add_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) : s + Metric.ball x δ = x +ᵥ Metric.thickening δ s

@[simp]

theorem div_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E) : s / Metric.ball x δ = x⁻¹ • Metric.thickening δ s

@[simp]

theorem sub_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) : s - Metric.ball x δ = -x +ᵥ Metric.thickening δ s

@[simp]

theorem ball_mul {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E) : Metric.ball x δ * s = x • Metric.thickening δ s

@[simp]

theorem ball_add {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) : Metric.ball x δ + s = x +ᵥ Metric.thickening δ s

@[simp]

theorem ball_div {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E) : Metric.ball x δ / s = x • Metric.thickening δ s⁻¹

@[simp]

theorem ball_sub {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) : Metric.ball x δ - s = x +ᵥ Metric.thickening δ (-s)

theorem IsCompact.mul_closedBall_one {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : s * Metric.closedBall 1 δ = Metric.cthickening δ s

theorem IsCompact.add_closedBall_zero {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : s + Metric.closedBall 0 δ = Metric.cthickening δ s

theorem IsCompact.div_closedBall_one {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : s / Metric.closedBall 1 δ = Metric.cthickening δ s

theorem IsCompact.sub_closedBall_zero {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : s - Metric.closedBall 0 δ = Metric.cthickening δ s

theorem IsCompact.closedBall_one_mul {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : Metric.closedBall 1 δ * s = Metric.cthickening δ s

theorem IsCompact.closedBall_zero_add {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : Metric.closedBall 0 δ + s = Metric.cthickening δ s

theorem IsCompact.closedBall_one_div {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : Metric.closedBall 1 δ / s = Metric.cthickening δ s⁻¹

theorem IsCompact.closedBall_zero_sub {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : Metric.closedBall 0 δ - s = Metric.cthickening δ (-s)

theorem IsCompact.mul_closedBall {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : s * Metric.closedBall x δ = x • Metric.cthickening δ s

theorem IsCompact.add_closedBall {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : s + Metric.closedBall x δ = x +ᵥ Metric.cthickening δ s

theorem IsCompact.div_closedBall {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : s / Metric.closedBall x δ = x⁻¹ • Metric.cthickening δ s

theorem IsCompact.sub_closedBall {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : s - Metric.closedBall x δ = -x +ᵥ Metric.cthickening δ s

theorem IsCompact.closedBall_mul {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : Metric.closedBall x δ * s = x • Metric.cthickening δ s

theorem IsCompact.closedBall_add {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : Metric.closedBall x δ + s = x +ᵥ Metric.cthickening δ s

theorem IsCompact.closedBall_div {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : Metric.closedBall x δ * s = x • Metric.cthickening δ s

theorem IsCompact.closedBall_sub {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : Metric.closedBall x δ + s = x +ᵥ Metric.cthickening δ s