mathlib3documentation

analysis.normed.group.pointwise

Properties of pointwise addition of sets in normed groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} {s t : set E} (hs : metric.bounded s) (ht : metric.bounded t) :
theorem metric.bounded.mul {E : Type u_1} {s t : set E} (hs : metric.bounded s) (ht : metric.bounded t) :
theorem metric.bounded.of_add {E : Type u_1} {s t : set E} (hst : metric.bounded (s + t)) :
theorem metric.bounded.of_mul {E : Type u_1} {s t : set E} (hst : metric.bounded (s * t)) :
theorem metric.bounded.inv {E : Type u_1} {s : set E} :
theorem metric.bounded.neg {E : Type u_1} {s : set E} :
theorem metric.bounded.div {E : Type u_1} {s t : set E} (hs : metric.bounded s) (ht : metric.bounded t) :
theorem metric.bounded.sub {E : Type u_1} {s t : set E} (hs : metric.bounded s) (ht : metric.bounded t) :
theorem inf_edist_neg {E : Type u_1} (x : E) (s : set E) :
s = (-s)
theorem inf_edist_inv {E : Type u_1} (x : E) (s : set E) :
@[simp]
theorem inf_edist_neg_neg {E : Type u_1} (x : E) (s : set E) :
(-s) =
@[simp]
theorem inf_edist_inv_inv {E : Type u_1} (x : E) (s : set E) :
theorem ediam_add_le {E : Type u_1} (x y : set E) :
theorem ediam_mul_le {E : Type u_1} (x y : set E) :
@[simp]
theorem inv_thickening {E : Type u_1} (δ : ) (s : set E) :
s)⁻¹ =
@[simp]
theorem neg_thickening {E : Type u_1} (δ : ) (s : set E) :
= (-s)
@[simp]
theorem inv_cthickening {E : Type u_1} (δ : ) (s : set E) :
@[simp]
theorem neg_cthickening {E : Type u_1} (δ : ) (s : set E) :
= (-s)
@[simp]
theorem neg_ball {E : Type u_1} (δ : ) (x : E) :
- δ = metric.ball (-x) δ
@[simp]
theorem inv_ball {E : Type u_1} (δ : ) (x : E) :
δ)⁻¹ =
@[simp]
theorem neg_closed_ball {E : Type u_1} (δ : ) (x : E) :
= δ
@[simp]
theorem inv_closed_ball {E : Type u_1} (δ : ) (x : E) :
theorem singleton_add_ball {E : Type u_1} (δ : ) (x y : E) :
{x} + δ = metric.ball (x + y) δ
theorem singleton_mul_ball {E : Type u_1} (δ : ) (x y : E) :
{x} * δ = metric.ball (x * y) δ
theorem singleton_sub_ball {E : Type u_1} (δ : ) (x y : E) :
{x} - δ = metric.ball (x - y) δ
theorem singleton_div_ball {E : Type u_1} (δ : ) (x y : E) :
{x} / δ = metric.ball (x / y) δ
theorem ball_mul_singleton {E : Type u_1} (δ : ) (x y : E) :
δ * {y} = metric.ball (x * y) δ
theorem ball_add_singleton {E : Type u_1} (δ : ) (x y : E) :
δ + {y} = metric.ball (x + y) δ
theorem ball_div_singleton {E : Type u_1} (δ : ) (x y : E) :
δ / {y} = metric.ball (x / y) δ
theorem ball_sub_singleton {E : Type u_1} (δ : ) (x y : E) :
δ - {y} = metric.ball (x - y) δ
theorem singleton_add_ball_zero {E : Type u_1} (δ : ) (x : E) :
{x} + δ = δ
theorem singleton_mul_ball_one {E : Type u_1} (δ : ) (x : E) :
{x} * δ = δ
theorem singleton_div_ball_one {E : Type u_1} (δ : ) (x : E) :
{x} / δ = δ
theorem singleton_sub_ball_zero {E : Type u_1} (δ : ) (x : E) :
{x} - δ = δ
theorem ball_zero_add_singleton {E : Type u_1} (δ : ) (x : E) :
δ + {x} = δ
theorem ball_one_mul_singleton {E : Type u_1} (δ : ) (x : E) :
δ * {x} = δ
theorem ball_one_div_singleton {E : Type u_1} (δ : ) (x : E) :
δ / {x} =
theorem ball_zero_sub_singleton {E : Type u_1} (δ : ) (x : E) :
δ - {x} = metric.ball (-x) δ
theorem vadd_ball_zero {E : Type u_1} (δ : ) (x : E) :
x +ᵥ δ = δ
theorem smul_ball_one {E : Type u_1} (δ : ) (x : E) :
x δ = δ
@[simp]
theorem singleton_mul_closed_ball {E : Type u_1} (δ : ) (x y : E) :
{x} * = metric.closed_ball (x * y) δ
@[simp]
theorem singleton_add_closed_ball {E : Type u_1} (δ : ) (x y : E) :
{x} + = metric.closed_ball (x + y) δ
@[simp]
theorem singleton_div_closed_ball {E : Type u_1} (δ : ) (x y : E) :
{x} / = metric.closed_ball (x / y) δ
@[simp]
theorem singleton_sub_closed_ball {E : Type u_1} (δ : ) (x y : E) :
{x} - = metric.closed_ball (x - y) δ
@[simp]
theorem closed_ball_add_singleton {E : Type u_1} (δ : ) (x y : E) :
+ {y} = metric.closed_ball (x + y) δ
@[simp]
theorem closed_ball_mul_singleton {E : Type u_1} (δ : ) (x y : E) :
* {y} = metric.closed_ball (x * y) δ
@[simp]
theorem closed_ball_sub_singleton {E : Type u_1} (δ : ) (x y : E) :
- {y} = metric.closed_ball (x - y) δ
@[simp]
theorem closed_ball_div_singleton {E : Type u_1} (δ : ) (x y : E) :
/ {y} = metric.closed_ball (x / y) δ
theorem singleton_add_closed_ball_zero {E : Type u_1} (δ : ) (x : E) :
{x} + =
theorem singleton_mul_closed_ball_one {E : Type u_1} (δ : ) (x : E) :
{x} * =
theorem singleton_div_closed_ball_one {E : Type u_1} (δ : ) (x : E) :
{x} / =
theorem singleton_sub_closed_ball_zero {E : Type u_1} (δ : ) (x : E) :
{x} - =
theorem closed_ball_one_mul_singleton {E : Type u_1} (δ : ) (x : E) :
* {x} =
theorem closed_ball_zero_add_singleton {E : Type u_1} (δ : ) (x : E) :
+ {x} =
theorem closed_ball_one_div_singleton {E : Type u_1} (δ : ) (x : E) :
/ {x} =
theorem closed_ball_zero_sub_singleton {E : Type u_1} (δ : ) (x : E) :
- {x} = δ
@[simp]
theorem vadd_closed_ball_zero {E : Type u_1} (δ : ) (x : E) :
x +ᵥ =
@[simp]
theorem smul_closed_ball_one {E : Type u_1} (δ : ) (x : E) :
x =
theorem mul_ball_one {E : Type u_1} (δ : ) (s : set E) :
s * δ =
theorem add_ball_zero {E : Type u_1} (δ : ) (s : set E) :
s + δ =
theorem sub_ball_zero {E : Type u_1} (δ : ) (s : set E) :
s - δ =
theorem div_ball_one {E : Type u_1} (δ : ) (s : set E) :
s / δ =
theorem ball_add_zero {E : Type u_1} (δ : ) (s : set E) :
δ + s =
theorem ball_mul_one {E : Type u_1} (δ : ) (s : set E) :
δ * s =
theorem ball_div_one {E : Type u_1} (δ : ) (s : set E) :
δ / s =
theorem ball_sub_zero {E : Type u_1} (δ : ) (s : set E) :
δ - s = (-s)
@[simp]
theorem add_ball {E : Type u_1} (δ : ) (s : set E) (x : E) :
s + δ = x +ᵥ
@[simp]
theorem mul_ball {E : Type u_1} (δ : ) (s : set E) (x : E) :
s * δ = x
@[simp]
theorem sub_ball {E : Type u_1} (δ : ) (s : set E) (x : E) :
s - δ = -x +ᵥ
@[simp]
theorem div_ball {E : Type u_1} (δ : ) (s : set E) (x : E) :
s / δ = x⁻¹
@[simp]
theorem ball_mul {E : Type u_1} (δ : ) (s : set E) (x : E) :
δ * s = x
@[simp]
theorem ball_add {E : Type u_1} (δ : ) (s : set E) (x : E) :
δ + s = x +ᵥ
@[simp]
theorem ball_div {E : Type u_1} (δ : ) (s : set E) (x : E) :
δ / s = x
@[simp]
theorem ball_sub {E : Type u_1} (δ : ) (s : set E) (x : E) :
δ - s = x +ᵥ (-s)
theorem is_compact.add_closed_ball_zero {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) :
s + =
theorem is_compact.mul_closed_ball_one {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) :
s * =
theorem is_compact.sub_closed_ball_zero {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) :
s - =
theorem is_compact.div_closed_ball_one {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) :
s / =
theorem is_compact.closed_ball_one_mul {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) :
* s =
theorem is_compact.closed_ball_zero_add {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) :
+ s =
theorem is_compact.closed_ball_zero_sub {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) :
- s = (-s)
theorem is_compact.closed_ball_one_div {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) :
/ s =
theorem is_compact.mul_closed_ball {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) (x : E) :
s * = x
theorem is_compact.add_closed_ball {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) (x : E) :
s + = x +ᵥ
theorem is_compact.sub_closed_ball {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) (x : E) :
s - =
theorem is_compact.div_closed_ball {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) (x : E) :
s / =
theorem is_compact.closed_ball_add {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) (x : E) :
+ s = x +ᵥ
theorem is_compact.closed_ball_mul {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) (x : E) :
* s = x
theorem is_compact.closed_ball_div {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) (x : E) :
* s = x
theorem is_compact.closed_ball_sub {E : Type u_1} {δ : } {s : set E} (hs : is_compact s) (hδ : 0 δ) (x : E) :
+ s = x +ᵥ