Documentation

Mathlib.Analysis.Normed.Group.Pointwise

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.mul {E : Type u_1} [SeminormedGroup E] {s t : Set E} (hs : IsBounded s) (ht : IsBounded t) :
IsBounded (s * t)
source
theorem Bornology.IsBounded.add {E : Type u_1} [SeminormedAddGroup E] {s t : Set E} (hs : IsBounded s) (ht : IsBounded t) :
IsBounded (s + t)
source
theorem Bornology.IsBounded.of_mul {E : Type u_1} [SeminormedGroup E] {s t : Set E} (hst : IsBounded (s * t)) :
IsBounded s ∨ IsBounded t
source
theorem Bornology.IsBounded.of_add {E : Type u_1} [SeminormedAddGroup E] {s t : Set E} (hst : IsBounded (s + t)) :
IsBounded s ∨ IsBounded t
source
theorem Bornology.IsBounded.inv {E : Type u_1} [SeminormedGroup E] {s : Set E} :
IsBounded s → IsBounded s⁻¹
source
theorem Bornology.IsBounded.neg {E : Type u_1} [SeminormedAddGroup E] {s : Set E} :
IsBounded s → IsBounded (-s)
source
theorem Bornology.IsBounded.div {E : Type u_1} [SeminormedGroup E] {s t : Set E} (hs : IsBounded s) (ht : IsBounded t) :
IsBounded (s / t)
source
theorem Bornology.IsBounded.sub {E : Type u_1} [SeminormedAddGroup E] {s t : Set E} (hs : IsBounded s) (ht : IsBounded t) :
IsBounded (s - t)
source
@[simp]
theorem infEDist_inv_inv {E : Type u_1} [SeminormedCommGroup E] (x : E) (s : Set E) :
Metric.infEDist x⁻¹ s⁻¹ = Metric.infEDist x s
source
@[simp]
theorem infEDist_neg_neg {E : Type u_1} [SeminormedAddCommGroup E] (x : E) (s : Set E) :
Metric.infEDist (-x) (-s) = Metric.infEDist x s
source
theorem infEDist_inv {E : Type u_1} [SeminormedCommGroup E] (x : E) (s : Set E) :
Metric.infEDist x⁻¹ s = Metric.infEDist x s⁻¹
source
theorem infEDist_neg {E : Type u_1} [SeminormedAddCommGroup E] (x : E) (s : Set E) :
Metric.infEDist (-x) s = Metric.infEDist x (-s)
source
theorem ediam_mul_le {E : Type u_1} [SeminormedCommGroup E] (x y : Set E) :
Metric.ediam (x * y) ≤ Metric.ediam x + Metric.ediam y
source
theorem ediam_add_le {E : Type u_1} [SeminormedAddCommGroup E] (x y : Set E) :
Metric.ediam (x + y) ≤ Metric.ediam x + Metric.ediam y
source
@[simp]
theorem inv_thickening {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) :
(Metric.thickening δ s)⁻¹ = Metric.thickening δ 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_cthickening {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) :
(Metric.cthickening δ s)⁻¹ = Metric.cthickening δ 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_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :
(Metric.ball x δ)⁻¹ = Metric.ball x⁻¹ δ
source
@[simp]
theorem neg_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
-Metric.ball x δ = Metric.ball (-x) δ
source
@[simp]
theorem inv_closedBall {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :
(Metric.closedBall x δ)⁻¹ = Metric.closedBall x⁻¹ δ
source
@[simp]
theorem neg_closedBall {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
-Metric.closedBall x δ = Metric.closedBall (-x) δ
source
@[simp]
theorem inv_sphere {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :
(Metric.sphere x δ)⁻¹ = Metric.sphere x⁻¹ δ
source
@[simp]
theorem neg_sphere {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
-Metric.sphere x δ = Metric.sphere (-x) δ
source
theorem singleton_mul_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) :
{x} * Metric.ball y δ = Metric.ball (x * y) δ
source
theorem singleton_add_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) :
{x} + Metric.ball y δ = Metric.ball (x + y) δ
source
theorem singleton_div_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) :
{x} / Metric.ball y δ = Metric.ball (x / y) δ
source
theorem singleton_sub_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) :
{x} - Metric.ball y δ = Metric.ball (x - y) δ
source
theorem ball_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) :
Metric.ball x δ * {y} = Metric.ball (x * y) δ
source
theorem ball_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) :
Metric.ball x δ + {y} = Metric.ball (x + y) δ
source
theorem ball_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) :
Metric.ball x δ / {y} = Metric.ball (x / y) δ
source
theorem ball_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) :
Metric.ball x δ - {y} = Metric.ball (x - y) δ
source
theorem singleton_mul_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :
{x} * Metric.ball 1 δ = Metric.ball x δ
source
theorem singleton_add_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 singleton_sub_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
{x} - Metric.ball 0 δ = 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_add_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 ball_zero_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
Metric.ball 0 δ - {x} = Metric.ball (-x) δ
source
theorem smul_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :
x • Metric.ball 1 δ = Metric.ball x δ
source
theorem vadd_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
x +ᵥ Metric.ball 0 δ = Metric.ball x δ
source
@[simp]
theorem singleton_mul_closedBall {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) :
{x} * Metric.closedBall y δ = Metric.closedBall (x * y) δ
source
@[simp]
theorem singleton_add_closedBall {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) :
{x} + Metric.closedBall y δ = Metric.closedBall (x + y) δ
source
@[simp]
theorem singleton_div_closedBall {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) :
{x} / Metric.closedBall y δ = Metric.closedBall (x / y) δ
source
@[simp]
theorem singleton_sub_closedBall {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) :
{x} - Metric.closedBall y δ = Metric.closedBall (x - y) δ
source
@[simp]
theorem closedBall_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) :
Metric.closedBall x δ * {y} = Metric.closedBall (x * y) δ
source
@[simp]
theorem closedBall_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) :
Metric.closedBall x δ + {y} = Metric.closedBall (x + y) δ
source
@[simp]
theorem closedBall_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) :
Metric.closedBall x δ / {y} = Metric.closedBall (x / y) δ
source
@[simp]
theorem closedBall_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) :
Metric.closedBall x δ - {y} = Metric.closedBall (x - y) δ
source
theorem singleton_mul_closedBall_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :
{x} * Metric.closedBall 1 δ = Metric.closedBall x δ
source
theorem singleton_add_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 singleton_sub_closedBall_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
{x} - Metric.closedBall 0 δ = 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_add_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
theorem closedBall_zero_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
Metric.closedBall 0 δ - {x} = 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
@[simp]
theorem vadd_closedBall_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
x +ᵥ Metric.closedBall 0 δ = Metric.closedBall x δ
source
@[simp]
theorem singleton_mul_sphere {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) :
{x} * Metric.sphere y δ = Metric.sphere (x * y) δ
source
@[simp]
theorem singleton_add_sphere {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) :
{x} + Metric.sphere y δ = Metric.sphere (x + y) δ
source
@[simp]
theorem singleton_div_sphere {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) :
{x} / Metric.sphere y δ = Metric.sphere (x / y) δ
source
@[simp]
theorem singleton_sub_sphere {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) :
{x} - Metric.sphere y δ = Metric.sphere (x - y) δ
source
@[simp]
theorem sphere_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) :
Metric.sphere x δ * {y} = Metric.sphere (x * y) δ
source
@[simp]
theorem sphere_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) :
Metric.sphere x δ + {y} = Metric.sphere (x + y) δ
source
@[simp]
theorem sphere_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) :
Metric.sphere x δ / {y} = Metric.sphere (x / y) δ
source
@[simp]
theorem sphere_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) :
Metric.sphere x δ - {y} = Metric.sphere (x - y) δ
source
theorem singleton_mul_sphere_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :
{x} * Metric.sphere 1 δ = Metric.sphere x δ
source
theorem singleton_add_sphere_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
{x} + Metric.sphere 0 δ = Metric.sphere x δ
source
theorem singleton_div_sphere_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :
{x} / Metric.sphere 1 δ = Metric.sphere x δ
source
theorem singleton_sub_sphere_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
{x} - Metric.sphere 0 δ = Metric.sphere x δ
source
theorem sphere_one_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :
Metric.sphere 1 δ * {x} = Metric.sphere x δ
source
theorem sphere_zero_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
Metric.sphere 0 δ + {x} = Metric.sphere x δ
source
theorem sphere_one_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :
Metric.sphere 1 δ / {x} = Metric.sphere x⁻¹ δ
source
theorem sphere_zero_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
Metric.sphere 0 δ - {x} = Metric.sphere (-x) δ
source
@[simp]
theorem smul_sphere_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) :
x • Metric.sphere 1 δ = Metric.sphere x δ
source
@[simp]
theorem vadd_sphere_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) :
x +ᵥ Metric.sphere 0 δ = Metric.sphere x δ
source
theorem mul_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) :
s * Metric.ball 1 δ = Metric.thickening δ s
source
theorem add_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 sub_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) :
s - Metric.ball 0 δ = 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_add_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
theorem ball_sub_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) :
Metric.ball 0 δ - s = 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 add_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 sub_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) :
s - Metric.ball x δ = -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_add {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
@[simp]
theorem ball_sub {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) :
Metric.ball x δ - s = x +ᵥ Metric.thickening δ (-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.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.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.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.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_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_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.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.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.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.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.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.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_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_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
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