no goals
α : Type ?u.46464
β : Type ?u.46467
γ : Type ?u.46470
ι : Type ?u.46473
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.46504
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (ball x r) = sphere x r
rw [frontier, closure_ball x hr, isOpen_ball.interior_eq, closedBall_diff_ball]