no goals
α : Type ?u.310915
β : Type ?u.310918
γ : Type ?u.310921
ι : Type ?u.310924
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.311017
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ frontier (sphere x r) = sphere x r
rw [isClosed_sphere.frontier_eq, interior_sphere' x, diff_empty]