Basic facts about real (semi)normed spaces

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

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} [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.

theorem inv_norm_smul_mem_unitClosedBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) : ‖x‖⁻¹ • x ∈ Metric.closedBall 0 1

theorem norm_smul_of_nonneg {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {t : ℝ} (ht : 0 ≤ t) (x : E) : ‖t • x‖ = t * ‖x‖

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

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

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

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

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

theorem interior_sphere {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) : interior (Metric.sphere x r) = ∅

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

theorem exists_norm_eq (E : Type u_1) [SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E] {c : ℝ} (hc : 0 ≤ c) : ∃ (x : E), ‖x‖ = c

@[simp]

theorem range_norm (E : Type u_1) [SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E] : Set.range norm = Set.Ici 0

theorem nnnorm_surjective (E : Type u_1) [SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E] : Function.Surjective nnnorm

@[simp]

theorem range_nnnorm (E : Type u_1) [SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E] : Set.range nnnorm = Set.univ

@[simp]

theorem NormedSpace.sphere_nonempty {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology 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.

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

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

@[simp]

theorem interior_sphere' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) : interior (Metric.sphere x r) = ∅

@[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