mathlib documentation

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 bounded_iff_exists_norm_le {E : Type u_1} [seminormed_add_comm_group E] {s : set E} :
metric.bounded s ↔ ∃ (R : ℝ), ∀ (x : E), x ∈ s → ∥x∥ ≤ R
source
theorem metric.bounded.exists_norm_le {E : Type u_1} [seminormed_add_comm_group E] {s : set E} :
metric.bounded s → (∃ (R : ℝ), ∀ (x : E), x ∈ s → ∥x∥ ≤ R)

Alias of the forward direction of bounded_iff_exists_norm_le.

source
theorem metric.bounded.exists_pos_norm_le {E : Type u_1} [seminormed_add_comm_group E] {s : set E} (hs : metric.bounded s) :
∃ (R : ℝ) (H : R > 0), ∀ (x : E), x ∈ s → ∥x∥ ≤ R
source
theorem metric.bounded.add {E : Type u_1} [seminormed_add_comm_group E] {s t : set E} (hs : metric.bounded s) (ht : metric.bounded t) :
metric.bounded (s + t)
source
theorem metric.bounded.neg {E : Type u_1} [seminormed_add_comm_group E] {s : set E} :
metric.bounded s → metric.bounded (-s)
source
theorem metric.bounded.sub {E : Type u_1} [seminormed_add_comm_group E] {s t : set E} (hs : metric.bounded s) (ht : metric.bounded t) :
metric.bounded (s - t)
source
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)
source
@[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
source
@[simp]
theorem neg_thickening {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (s : set E) :
-metric.thickening δ s = metric.thickening δ (-s)
source
@[simp]
theorem neg_cthickening {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (s : set E) :
-metric.cthickening δ s = metric.cthickening δ (-s)
source
@[simp]
theorem neg_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (x : E) :
-metric.ball x δ = metric.ball (-x) δ
source
@[simp]
theorem neg_closed_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (x : E) :
-metric.closed_ball x δ = metric.closed_ball (-x) δ
source
theorem singleton_add_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (x y : E) :
{x} + metric.ball y δ = metric.ball (x + y) δ
source
theorem singleton_sub_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (x y : E) :
{x} - metric.ball y δ = metric.ball (x - y) δ
source
theorem ball_add_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (x y : E) :
metric.ball x δ + {y} = metric.ball (x + y) δ
source
theorem ball_sub_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (x y : E) :
metric.ball x δ - {y} = metric.ball (x - y) δ
source
theorem singleton_add_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (x : E) :
{x} + metric.ball 0 δ = metric.ball x δ
source
theorem singleton_sub_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (x : E) :
{x} - metric.ball 0 δ = metric.ball x δ
source
theorem ball_zero_add_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (x : E) :
metric.ball 0 δ + {x} = metric.ball x δ
source
theorem ball_zero_sub_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (x : E) :
metric.ball 0 δ - {x} = metric.ball (-x) δ
source
theorem vadd_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (x : E) :
x +ᵥ metric.ball 0 δ = metric.ball x δ
source
@[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) δ
source
@[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) δ
source
@[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) δ
source
@[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) δ
source
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 δ
source
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 δ
source
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 δ
source
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) δ
source
@[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 δ
source
theorem add_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (s : set E) :
s + metric.ball 0 δ = metric.thickening δ s
source
theorem sub_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (s : set E) :
s - metric.ball 0 δ = metric.thickening δ s
source
theorem ball_add_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (s : set E) :
metric.ball 0 δ + s = metric.thickening δ s
source
theorem ball_sub_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ℝ) (s : set E) :
metric.ball 0 δ - s = metric.thickening δ (-s)
source
@[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
source
@[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
source
@[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
source
@[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)
source
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
source
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
source
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
source
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)
source
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
source
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
source
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
source
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