# Basic facts about real (semi)normed spaces #

In this file we prove some theorems about (semi)normed spaces over real numberes.

## Main results #

- `closure_ball`, `frontier_ball`, `interior_closedBall`, `frontier_closedBall`, `interior_sphere`, `frontier_sphere`: formulas for the closure/interior/frontier of nontrivial balls and spheres in a real seminormed space;

- `interior_closedBall'`, `frontier_closedBall'`, `interior_sphere'`, `frontier_sphere'`: similar lemmas assuming that the ambient space is separated and nontrivial instead of `r ≠ 0`.

source
instance Real.punctured_nhds_module_neBot {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [ContinuousAdd E] [Nontrivial E] [Module ℝ E] [ContinuousSMul ℝ E] (x : E) :
(nhdsWithin x {x}ᶜ).NeBot

If `E` is a nontrivial topological module over `ℝ`, then `E` has no isolated points. This is a particular case of `Module.punctured_nhds_neBot`.

source
theorem inv_norm_smul_mem_unitClosedBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) :
‖x‖⁻¹ • x ∈ Metric.closedBall 0 1
source
theorem norm_smul_of_nonneg {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {t : ℝ} (ht : 0 ≤ t) (x : E) :
‖t • x‖ = t * ‖x‖
source
theorem dist_smul_add_one_sub_smul_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} {x y : E} (h : r ∈ Set.Icc 0 1) :
dist (r • x + (1 - r) • y) x ≤ dist y x
source
theorem closure_ball {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :
closure (Metric.ball x r) = Metric.closedBall x r
source
theorem frontier_ball {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :
frontier (Metric.ball x r) = Metric.sphere x r
source
theorem interior_closedBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :
interior (Metric.closedBall x r) = Metric.ball x r
source
theorem frontier_closedBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :
frontier (Metric.closedBall x r) = Metric.sphere x r
source
theorem interior_sphere {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :
interior (Metric.sphere x r) = ∅
source
theorem frontier_sphere {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :
frontier (Metric.sphere x r) = Metric.sphere x r
source
theorem exists_norm_eq (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {c : ℝ} (hc : 0 ≤ c) :
∃ (x : E), ‖x‖ = c
source
@[simp]
theorem range_norm (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] :
Set.range norm = Set.Ici 0
source
theorem nnnorm_surjective (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] :
Function.Surjective nnnorm
source
@[simp]
theorem range_nnnorm (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] :
Set.range nnnorm = Set.univ
source
@[simp]
theorem NormedSpace.sphere_nonempty {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {x : E} {r : ℝ} :
(Metric.sphere x r).Nonempty ↔ 0 ≤ r

In a nontrivial real normed space, a sphere is nonempty if and only if its radius is nonnegative.

source
theorem interior_closedBall' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) :
interior (Metric.closedBall x r) = Metric.ball x r
source
theorem frontier_closedBall' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) :
frontier (Metric.closedBall x r) = Metric.sphere x r
source
@[simp]
theorem interior_sphere' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) :
interior (Metric.sphere x r) = ∅
source
@[simp]
theorem frontier_sphere' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) :
frontier (Metric.sphere x r) = Metric.sphere x r