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 metric.bounded.add {E : Type u_1} [seminormed_add_group E] {s t : set E} (hs : metric.bounded s) (ht : metric.bounded t) :
theorem metric.bounded.mul {E : Type u_1} [seminormed_group E] {s t : set E} (hs : metric.bounded s) (ht : metric.bounded t) :
theorem metric.bounded.div {E : Type u_1} [seminormed_group E] {s t : set E} (hs : metric.bounded s) (ht : metric.bounded t) :
theorem metric.bounded.sub {E : Type u_1} [seminormed_add_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]
@[simp]
theorem inv_thickening {E : Type u_1} [seminormed_comm_group E] (δ : ) (s : set E) :
@[simp]
theorem neg_thickening {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (s : set E) :
@[simp]
@[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 inv_ball {E : Type u_1} [seminormed_comm_group E] (δ : ) (x : E) :
@[simp]
theorem neg_closed_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x : E) :
@[simp]
theorem inv_closed_ball {E : Type u_1} [seminormed_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_mul_ball {E : Type u_1} [seminormed_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 singleton_div_ball {E : Type u_1} [seminormed_comm_group E] (δ : ) (x y : E) :
{x} / metric.ball y δ = metric.ball (x / y) δ
theorem ball_mul_singleton {E : Type u_1} [seminormed_comm_group E] (δ : ) (x y : E) :
metric.ball x δ * {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_div_singleton {E : Type u_1} [seminormed_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_mul_ball_one {E : Type u_1} [seminormed_comm_group E] (δ : ) (x : E) :
{x} * metric.ball 1 δ = metric.ball x δ
theorem singleton_div_ball_one {E : Type u_1} [seminormed_comm_group E] (δ : ) (x : E) :
{x} / metric.ball 1 δ = 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_one_mul_singleton {E : Type u_1} [seminormed_comm_group E] (δ : ) (x : E) :
metric.ball 1 δ * {x} = metric.ball x δ
theorem ball_one_div_singleton {E : Type u_1} [seminormed_comm_group E] (δ : ) (x : E) :
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) :
theorem smul_ball_one {E : Type u_1} [seminormed_comm_group E] (δ : ) (x : E) :
@[simp]
theorem singleton_mul_closed_ball {E : Type u_1} [seminormed_comm_group E] (δ : ) (x y : E) :
@[simp]
theorem singleton_add_closed_ball {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x y : E) :
@[simp]
theorem singleton_div_closed_ball {E : Type u_1} [seminormed_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_mul_singleton {E : Type u_1} [seminormed_comm_group E] (δ : ) (x y : E) :
@[simp]
theorem closed_ball_sub_singleton {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (x y : E) :
@[simp]
theorem closed_ball_div_singleton {E : Type u_1} [seminormed_comm_group E] (δ : ) (x y : E) :
@[simp]
@[simp]
theorem smul_closed_ball_one {E : Type u_1} [seminormed_comm_group E] (δ : ) (x : E) :
theorem mul_ball_one {E : Type u_1} [seminormed_comm_group E] (δ : ) (s : set 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 div_ball_one {E : Type u_1} [seminormed_comm_group E] (δ : ) (s : set E) :
theorem ball_add_zero {E : Type u_1} [seminormed_add_comm_group E] (δ : ) (s : set E) :
theorem ball_mul_one {E : Type u_1} [seminormed_comm_group E] (δ : ) (s : set E) :
theorem ball_div_one {E : Type u_1} [seminormed_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 mul_ball {E : Type u_1} [seminormed_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 div_ball {E : Type u_1} [seminormed_comm_group E] (δ : ) (s : set E) (x : E) :
@[simp]
theorem ball_mul {E : Type u_1} [seminormed_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_div {E : Type u_1} [seminormed_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.mul_closed_ball_one {E : Type u_1} [seminormed_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.div_closed_ball_one {E : Type u_1} [seminormed_comm_group E] {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) :
theorem is_compact.closed_ball_one_mul {E : Type u_1} [seminormed_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.closed_ball_one_div {E : Type u_1} [seminormed_comm_group E] {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) :
theorem is_compact.mul_closed_ball {E : Type u_1} [seminormed_comm_group E] {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) (x : E) :
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.div_closed_ball {E : Type u_1} [seminormed_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_mul {E : Type u_1} [seminormed_comm_group E] {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) (x : E) :
theorem is_compact.closed_ball_div {E : Type u_1} [seminormed_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) :