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.

source

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

Bornology.IsBounded (s + t)

source

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

Bornology.IsBounded (s * t)

source

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

Bornology.IsBounded s → Bornology.IsBounded (-s)

source

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

Bornology.IsBounded s → Bornology.IsBounded s⁻¹

source

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

Bornology.IsBounded (s - t)

source

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

Bornology.IsBounded (s / t)

source

@[simp]

theorem infEdist_neg_neg {E : Type u_1} [SeminormedAddCommGroup E] (x : E) (s : Set E) :

EMetric.infEdist (-x) (-s) = EMetric.infEdist x s

source

@[simp]

theorem infEdist_inv_inv {E : Type u_1} [SeminormedCommGroup E] (x : E) (s : Set E) :

EMetric.infEdist x⁻¹ s⁻¹ = EMetric.infEdist x s

source

theorem infEdist_neg {E : Type u_1} [SeminormedAddCommGroup E] (x : E) (s : Set E) :

EMetric.infEdist (-x) s = EMetric.infEdist x (-s)

source

theorem infEdist_inv {E : Type u_1} [SeminormedCommGroup E] (x : E) (s : Set E) :

EMetric.infEdist x⁻¹ s = EMetric.infEdist x s⁻¹

source

@[simp]

theorem neg_thickening {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) :

-Metric.thickening δ s = Metric.thickening δ (-s)

source

@[simp]

theorem inv_thickening {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) :

(Metric.thickening δ s)⁻¹ = Metric.thickening δ s⁻¹

source

@[simp]

theorem neg_cthickening {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) :

-Metric.cthickening δ s = Metric.cthickening δ (-s)

source

@[simp]

theorem inv_cthickening {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) :

(Metric.cthickening δ s)⁻¹ = Metric.cthickening δ s⁻¹

source

@[simp]

theorem neg_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :

-Metric.ball x δ = Metric.ball (-x) δ

source

@[simp]

theorem inv_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :

(Metric.ball x δ)⁻¹ = Metric.ball x⁻¹ δ

source

@[simp]

theorem neg_closedBall {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :

-Metric.closedBall x δ = Metric.closedBall (-x) δ

source

@[simp]

theorem inv_closedBall {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :

(Metric.closedBall x δ)⁻¹ = Metric.closedBall x⁻¹ δ

source

theorem singleton_add_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) (y : E) :

{x} + Metric.ball y δ = Metric.ball (x + y) δ

source

theorem singleton_mul_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) (y : E) :

{x} * Metric.ball y δ = Metric.ball (x * y) δ

source

theorem singleton_sub_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) (y : E) :

{x} - Metric.ball y δ = Metric.ball (x - y) δ

source

theorem singleton_div_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) (y : E) :

{x} / Metric.ball y δ = Metric.ball (x / y) δ

source

theorem ball_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) (y : E) :

Metric.ball x δ + {y} = Metric.ball (x + y) δ

source

theorem ball_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) (y : E) :

Metric.ball x δ * {y} = Metric.ball (x * y) δ

source

theorem ball_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) (y : E) :

Metric.ball x δ - {y} = Metric.ball (x - y) δ

source

theorem ball_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) (y : E) :

Metric.ball x δ / {y} = Metric.ball (x / y) δ

source

theorem singleton_add_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :

{x} + Metric.ball 0 δ = Metric.ball x δ

source

theorem singleton_mul_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :

{x} * Metric.ball 1 δ = Metric.ball x δ

source

theorem singleton_sub_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :

{x} - Metric.ball 0 δ = Metric.ball x δ

source

theorem singleton_div_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :

{x} / Metric.ball 1 δ = Metric.ball x δ

source

theorem ball_zero_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :

Metric.ball 0 δ + {x} = Metric.ball x δ

source

theorem ball_one_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :

Metric.ball 1 δ * {x} = Metric.ball x δ

source

theorem ball_zero_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :

Metric.ball 0 δ - {x} = Metric.ball (-x) δ

source

theorem ball_one_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :

Metric.ball 1 δ / {x} = Metric.ball x⁻¹ δ

source

theorem vadd_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :

x +ᵥ Metric.ball 0 δ = Metric.ball x δ

source

theorem smul_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :

x • Metric.ball 1 δ = Metric.ball x δ

source

@[simp]

theorem singleton_add_closedBall {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) (y : E) :

{x} + Metric.closedBall y δ = Metric.closedBall (x + y) δ

source

@[simp]

theorem singleton_mul_closedBall {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) (y : E) :

{x} * Metric.closedBall y δ = Metric.closedBall (x * y) δ

source

@[simp]

theorem singleton_sub_closedBall {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) (y : E) :

{x} - Metric.closedBall y δ = Metric.closedBall (x - y) δ

source

@[simp]

theorem singleton_div_closedBall {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) (y : E) :

{x} / Metric.closedBall y δ = Metric.closedBall (x / y) δ

source

@[simp]

theorem closedBall_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) (y : E) :

Metric.closedBall x δ + {y} = Metric.closedBall (x + y) δ

source

@[simp]

theorem closedBall_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) (y : E) :

Metric.closedBall x δ * {y} = Metric.closedBall (x * y) δ

source

@[simp]

theorem closedBall_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) (y : E) :

Metric.closedBall x δ - {y} = Metric.closedBall (x - y) δ

source

@[simp]

theorem closedBall_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) (y : E) :

Metric.closedBall x δ / {y} = Metric.closedBall (x / y) δ

source

theorem singleton_add_closedBall_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :

{x} + Metric.closedBall 0 δ = Metric.closedBall x δ

source

theorem singleton_mul_closedBall_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :

{x} * Metric.closedBall 1 δ = Metric.closedBall x δ

source

theorem singleton_sub_closedBall_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :

{x} - Metric.closedBall 0 δ = Metric.closedBall x δ

source

theorem singleton_div_closedBall_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :

{x} / Metric.closedBall 1 δ = Metric.closedBall x δ

source

theorem closedBall_zero_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :

Metric.closedBall 0 δ + {x} = Metric.closedBall x δ

source

theorem closedBall_one_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :

Metric.closedBall 1 δ * {x} = Metric.closedBall x δ

source

theorem closedBall_zero_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :

Metric.closedBall 0 δ - {x} = Metric.closedBall (-x) δ

source

theorem closedBall_one_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :

Metric.closedBall 1 δ / {x} = Metric.closedBall x⁻¹ δ

source

@[simp]

theorem vadd_closedBall_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :

x +ᵥ Metric.closedBall 0 δ = Metric.closedBall x δ

source

@[simp]

theorem smul_closedBall_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :

x • Metric.closedBall 1 δ = Metric.closedBall x δ

source

theorem add_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) :

s + Metric.ball 0 δ = Metric.thickening δ s

source

theorem mul_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) :

s * Metric.ball 1 δ = Metric.thickening δ s

source

theorem sub_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) :

s - Metric.ball 0 δ = Metric.thickening δ s

source

theorem div_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) :

s / Metric.ball 1 δ = Metric.thickening δ s

source

theorem ball_add_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) :

Metric.ball 0 δ + s = Metric.thickening δ s

source

theorem ball_mul_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) :

Metric.ball 1 δ * s = Metric.thickening δ s

source

theorem ball_sub_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) :

Metric.ball 0 δ - s = Metric.thickening δ (-s)

source

theorem ball_div_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) :

Metric.ball 1 δ / s = Metric.thickening δ s⁻¹

source

@[simp]

theorem add_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) :

s + Metric.ball x δ = x +ᵥ Metric.thickening δ s

source

@[simp]

theorem mul_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E) :

s * Metric.ball x δ = x • Metric.thickening δ s

source

@[simp]

theorem sub_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) :

s - Metric.ball x δ = -x +ᵥ Metric.thickening δ s

source

@[simp]

theorem div_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E) :

s / Metric.ball x δ = x⁻¹ • Metric.thickening δ s

source

@[simp]

theorem ball_add {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) :

Metric.ball x δ + s = x +ᵥ Metric.thickening δ s

source

@[simp]

theorem ball_mul {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E) :

Metric.ball x δ * s = x • Metric.thickening δ s

source

@[simp]

theorem ball_sub {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) :

Metric.ball x δ - s = x +ᵥ Metric.thickening δ (-s)

source

@[simp]

theorem ball_div {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E) :

Metric.ball x δ / s = x • Metric.thickening δ s⁻¹

source

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

source

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

source

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

source

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

source

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

source

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

source

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)

source

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⁻¹

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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