no goals
α : Type ?u.309886
β : Type ?u.309889
γ : Type ?u.309892
ι : Type ?u.309895
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.309988
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ interior (sphere x r) = ∅
rw [← frontier_closedBall' x, interior_frontier isClosed_ball]