chore: forward-port leanprover-community/mathlib#18869 (#3676)

Mathlib/Analysis/NormedSpace/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Johannes Hölzl
 
 ! This file was ported from Lean 3 source module analysis.normed_space.basic
-! leanprover-community/mathlib commit d3af0609f6db8691dffdc3e1fb7feb7da72698f2
+! leanprover-community/mathlib commit 8000bbbe2e9d39b84edb993d88781f536a8a3fa8
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -203,6 +203,16 @@ theorem frontier_closedBall [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0)
   rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_diff_ball]
 #align frontier_closed_ball frontier_closedBall
 
+theorem interior_sphere [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :
+    interior (sphere x r) = ∅ := by
+  rw [← frontier_closedBall x hr, interior_frontier isClosed_ball]
+#align interior_sphere interior_sphere
+
+theorem frontier_sphere [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :
+    frontier (sphere x r) = sphere x r := by
+  rw [isClosed_sphere.frontier_eq, interior_sphere x hr, diff_empty]
+#align frontier_sphere frontier_sphere
+
 instance {E : Type _} [NormedAddCommGroup E] [NormedSpace ℚ E] (e : E) :
     DiscreteTopology <| AddSubgroup.zmultiples e := by
   rcases eq_or_ne e 0 with (rfl | he)
@@ -430,6 +440,17 @@ theorem frontier_closedBall' [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ
   rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_diff_ball]
 #align frontier_closed_ball' frontier_closedBall'
 
+@[simp]
+theorem interior_sphere' [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) :
+    interior (sphere x r) = ∅ := by rw [← frontier_closedBall' x, interior_frontier isClosed_ball]
+#align interior_sphere' interior_sphere'
+
+@[simp]
+theorem frontier_sphere' [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) :
+    frontier (sphere x r) = sphere x r := by
+  rw [isClosed_sphere.frontier_eq, interior_sphere' x, diff_empty]
+#align frontier_sphere' frontier_sphere'
+
 theorem rescale_to_shell_zpow {c : α} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : x ≠ 0) :
     ∃ n : ℤ, c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖ :=
   rescale_to_shell_semi_normed_zpow hc εpos (mt norm_eq_zero.1 hx)

Mathlib/Topology/MetricSpace/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis, Johannes Hölzl, Mario Carneiro, Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module topology.metric_space.basic
-! leanprover-community/mathlib commit 195fcd60ff2bfe392543bceb0ec2adcdb472db4c
+! leanprover-community/mathlib commit 8000bbbe2e9d39b84edb993d88781f536a8a3fa8
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1872,6 +1872,11 @@ theorem closure_closedBall : closure (closedBall x ε) = closedBall x ε :=
   isClosed_ball.closure_eq
 #align metric.closure_closed_ball Metric.closure_closedBall
 
+@[simp]
+theorem closure_sphere : closure (sphere x ε) = sphere x ε :=
+  isClosed_sphere.closure_eq
+#align metric.closure_sphere Metric.closure_sphere
+
 theorem closure_ball_subset_closedBall : closure (ball x ε) ⊆ closedBall x ε :=
   closure_minimal ball_subset_closedBall isClosed_ball
 #align metric.closure_ball_subset_closed_ball Metric.closure_ball_subset_closedBall