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.

@[simp]
theorem infEdist_neg_neg {E : Type u_1} [SeminormedAddCommGroup E] (x : E) (s : Set E) :
@[simp]
theorem infEdist_neg {E : Type u_1} [SeminormedAddCommGroup E] (x : E) (s : Set E) :
@[simp]
theorem neg_thickening {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (s : Set E) :
@[simp]
@[simp]
@[simp]
@[simp]
theorem neg_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) :
@[simp]
theorem inv_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) :
@[simp]
theorem neg_closedBall {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) :
@[simp]
theorem singleton_add_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) (y : E) :
{x} + Metric.ball y δ = Metric.ball (x + y) δ
theorem singleton_mul_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) (y : E) :
{x} * Metric.ball y δ = Metric.ball (x * y) δ
theorem singleton_sub_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) (y : E) :
{x} - Metric.ball y δ = Metric.ball (x - y) δ
theorem singleton_div_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) (y : E) :
{x} / Metric.ball y δ = Metric.ball (x / y) δ
theorem ball_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) (y : E) :
Metric.ball x δ + {y} = Metric.ball (x + y) δ
theorem ball_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) (y : E) :
Metric.ball x δ * {y} = Metric.ball (x * y) δ
theorem ball_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) (y : E) :
Metric.ball x δ - {y} = Metric.ball (x - y) δ
theorem ball_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) (y : E) :
Metric.ball x δ / {y} = Metric.ball (x / y) δ
theorem singleton_add_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) :
{x} + Metric.ball 0 δ = Metric.ball x δ
theorem singleton_mul_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) :
{x} * Metric.ball 1 δ = Metric.ball x δ
theorem singleton_sub_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) :
{x} - Metric.ball 0 δ = Metric.ball x δ
theorem singleton_div_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) :
{x} / Metric.ball 1 δ = Metric.ball x δ
theorem ball_zero_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) :
Metric.ball 0 δ + {x} = Metric.ball x δ
theorem ball_one_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) :
Metric.ball 1 δ * {x} = Metric.ball x δ
theorem ball_zero_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) :
Metric.ball 0 δ - {x} = Metric.ball (-x) δ
theorem ball_one_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) :
theorem vadd_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) :
theorem smul_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) :
@[simp]
theorem singleton_add_closedBall {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) (y : E) :
@[simp]
theorem singleton_mul_closedBall {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) (y : E) :
@[simp]
theorem singleton_sub_closedBall {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) (y : E) :
@[simp]
theorem singleton_div_closedBall {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) (y : E) :
@[simp]
theorem closedBall_add_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) (y : E) :
@[simp]
theorem closedBall_mul_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) (y : E) :
@[simp]
theorem closedBall_sub_singleton {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (x : E) (y : E) :
@[simp]
theorem closedBall_div_singleton {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) (y : E) :
@[simp]
@[simp]
theorem smul_closedBall_one {E : Type u_1} [SeminormedCommGroup E] (δ : ) (x : E) :
theorem add_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (s : Set E) :
theorem mul_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ) (s : Set E) :
theorem sub_ball_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (s : Set E) :
theorem div_ball_one {E : Type u_1} [SeminormedCommGroup E] (δ : ) (s : Set E) :
theorem ball_add_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (s : Set E) :
theorem ball_mul_one {E : Type u_1} [SeminormedCommGroup E] (δ : ) (s : Set E) :
theorem ball_sub_zero {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (s : Set E) :
theorem ball_div_one {E : Type u_1} [SeminormedCommGroup E] (δ : ) (s : Set E) :
@[simp]
theorem add_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (s : Set E) (x : E) :
@[simp]
theorem mul_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ) (s : Set E) (x : E) :
@[simp]
theorem sub_ball {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (s : Set E) (x : E) :
@[simp]
theorem div_ball {E : Type u_1} [SeminormedCommGroup E] (δ : ) (s : Set E) (x : E) :
@[simp]
theorem ball_add {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (s : Set E) (x : E) :
@[simp]
theorem ball_mul {E : Type u_1} [SeminormedCommGroup E] (δ : ) (s : Set E) (x : E) :
@[simp]
theorem ball_sub {E : Type u_1} [SeminormedAddCommGroup E] (δ : ) (s : Set E) (x : E) :
@[simp]
theorem ball_div {E : Type u_1} [SeminormedCommGroup E] (δ : ) (s : Set E) (x : E) :
theorem IsCompact.add_closedBall_zero {E : Type u_1} [SeminormedAddCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) :
theorem IsCompact.mul_closedBall_one {E : Type u_1} [SeminormedCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) :
theorem IsCompact.sub_closedBall_zero {E : Type u_1} [SeminormedAddCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) :
theorem IsCompact.div_closedBall_one {E : Type u_1} [SeminormedCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) :
theorem IsCompact.closedBall_zero_add {E : Type u_1} [SeminormedAddCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) :
theorem IsCompact.closedBall_one_mul {E : Type u_1} [SeminormedCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) :
theorem IsCompact.closedBall_zero_sub {E : Type u_1} [SeminormedAddCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) :
theorem IsCompact.closedBall_one_div {E : Type u_1} [SeminormedCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) :
theorem IsCompact.add_closedBall {E : Type u_1} [SeminormedAddCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) (x : E) :
theorem IsCompact.mul_closedBall {E : Type u_1} [SeminormedCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) (x : E) :
theorem IsCompact.sub_closedBall {E : Type u_1} [SeminormedAddCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) (x : E) :
theorem IsCompact.div_closedBall {E : Type u_1} [SeminormedCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) (x : E) :
theorem IsCompact.closedBall_add {E : Type u_1} [SeminormedAddCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) (x : E) :
theorem IsCompact.closedBall_mul {E : Type u_1} [SeminormedCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) (x : E) :
theorem IsCompact.closedBall_sub {E : Type u_1} [SeminormedAddCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) (x : E) :
theorem IsCompact.closedBall_div {E : Type u_1} [SeminormedCommGroup E] {δ : } {s : Set E} (hs : IsCompact s) (hδ : 0 δ) (x : E) :