no goals
α : Type ?u.89830
β : Type ?u.89833
γ : Type ?u.89836
ι : Type ?u.89839
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.89870
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (sphere x r) = ∅
rw [← frontier_closedBall x hr, interior_frontier isClosed_ball]