no goals
α : Type ?u.90652
β : Type ?u.90655
γ : Type ?u.90658
ι : Type ?u.90661
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.90692
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (sphere x r) = sphere x r
rw [isClosed_sphere.frontier_eq, interior_sphere x hr, diff_empty]