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.

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 sx R
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 sx R)

Alias of the forward direction of bounded_iff_exists_norm_le.

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 sx R
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) :
theorem metric.bounded.neg {E : Type u_1} [seminormed_add_comm_group E] {s : set E} :
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) :
theorem inf_edist_neg {E : Type u_1} [seminormed_add_comm_group E] (x : E) (s : set E) :
@[simp]
theorem inf_edist_neg_neg {E : Type u_1} [seminormed_add_comm_group E] (x : E) (s : set E) :
@[simp]
theorem neg_thickening {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (s : set E) :
@[simp]
theorem neg_cthickening {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (s : set E) :
@[simp]
theorem neg_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
@[simp]
theorem neg_closed_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
theorem singleton_add_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x y : E) :
{x} + metric.ball y δ = metric.ball (x + y) δ
theorem singleton_sub_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x y : E) :
{x} - metric.ball y δ = metric.ball (x - y) δ
theorem ball_add_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x y : E) :
metric.ball x δ + {y} = metric.ball (x + y) δ
theorem ball_sub_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x y : E) :
metric.ball x δ - {y} = metric.ball (x - y) δ
theorem singleton_add_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
{x} + metric.ball 0 δ = metric.ball x δ
theorem singleton_sub_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
{x} - metric.ball 0 δ = metric.ball x δ
theorem ball_zero_add_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
metric.ball 0 δ + {x} = metric.ball x δ
theorem ball_zero_sub_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
metric.ball 0 δ - {x} = metric.ball (-x) δ
theorem vadd_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
@[simp]
theorem singleton_add_closed_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x y : E) :
@[simp]
theorem singleton_sub_closed_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x y : E) :
@[simp]
theorem closed_ball_add_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x y : E) :
@[simp]
theorem closed_ball_sub_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x y : E) :
theorem singleton_add_closed_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
theorem singleton_sub_closed_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
theorem closed_ball_zero_add_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
theorem closed_ball_zero_sub_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
@[simp]
theorem vadd_closed_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
theorem add_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (s : set E) :
theorem sub_ball_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (s : set E) :
theorem ball_add_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (s : set E) :
theorem ball_sub_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (s : set E) :
@[simp]
theorem add_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (s : set E) (x : E) :
@[simp]
theorem sub_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (s : set E) (x : E) :
@[simp]
theorem ball_add {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (s : set E) (x : E) :
@[simp]
theorem ball_sub {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (s : set E) (x : E) :
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 δ) :
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 δ) :
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 δ) :
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 δ) :
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) :
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) :
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) :
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) :