# 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.

instance Real.punctured_nhds_module_neBot {E : Type u_1} [] [] [] [] [] [] (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.

Equations
• =
theorem norm_smul_of_nonneg {E : Type u_1} [] {t : } (ht : 0 t) (x : E) :
theorem dist_smul_add_one_sub_smul_le {E : Type u_1} [] {r : } {x : E} {y : E} (h : r Set.Icc 0 1) :
dist (r x + (1 - r) y) x dist y x
theorem closure_ball {E : Type u_1} [] (x : E) {r : } (hr : r 0) :
theorem frontier_ball {E : Type u_1} [] (x : E) {r : } (hr : r 0) :
theorem interior_closedBall {E : Type u_1} [] (x : E) {r : } (hr : r 0) :
=
theorem frontier_closedBall {E : Type u_1} [] (x : E) {r : } (hr : r 0) :
=
theorem interior_sphere {E : Type u_1} [] (x : E) {r : } (hr : r 0) :
theorem frontier_sphere {E : Type u_1} [] (x : E) {r : } (hr : r 0) :
theorem exists_norm_eq (E : Type u_1) [] [] {c : } (hc : 0 c) :
∃ (x : E), x = c
@[simp]
theorem range_norm (E : Type u_1) [] [] :
Set.range norm =
theorem nnnorm_surjective (E : Type u_1) [] [] :
@[simp]
theorem range_nnnorm (E : Type u_1) [] [] :
Set.range nnnorm = Set.univ
theorem interior_closedBall' {E : Type u_1} [] [] (x : E) (r : ) :
=
theorem frontier_closedBall' {E : Type u_1} [] [] (x : E) (r : ) :
=
@[simp]
theorem interior_sphere' {E : Type u_1} [] [] (x : E) (r : ) :
@[simp]
theorem frontier_sphere' {E : Type u_1} [] [] (x : E) (r : ) :