no goals
α : Type ?u.308974
β : Type ?u.308977
γ : Type ?u.308980
ι : Type ?u.308983
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.309076
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ frontier (closedBall x r) = sphere x r
rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_diff_ball]