no goals
α : Type ?u.89099
β : Type ?u.89102
γ : Type ?u.89105
ι : Type ?u.89108
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.89139
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (closedBall x r) = sphere x r
rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_diff_ball]