case inl
F : Type ?u.119922
α : Type ?u.119925
β : Type ?u.119928
𝕜 : Type ?u.119931
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ AddSalemSpencer (sphere x 0)

case inr
F : Type ?u.119922
α : Type ?u.119925
β : Type ?u.119928
𝕜 : Type ?u.119931
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ AddSalemSpencer (sphere x r)
F : Type ?u.119922
α : Type ?u.119925
β : Type ?u.119928
𝕜 : Type ?u.119931
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
⊢ AddSalemSpencer (sphere x r)
obtain rfl | hr := eq_or_ne r 0
case inl
F : Type ?u.119922
α : Type ?u.119925
β : Type ?u.119928
𝕜 : Type ?u.119931
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ AddSalemSpencer {x}
case inl
F : Type ?u.119922
α : Type ?u.119925
β : Type ?u.119928
𝕜 : Type ?u.119931
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ AddSalemSpencer (sphere x 0)
rw [sphere_zero]
no goals
case inl
F : Type ?u.119922
α : Type ?u.119925
β : Type ?u.119928
𝕜 : Type ?u.119931
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ AddSalemSpencer {x}
exact addSalemSpencer_singleton _
case h.e'_3
F : Type ?u.119922
α : Type ?u.119925
β : Type ?u.119928
𝕜 : Type ?u.119931
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ sphere x r = frontier (closedBall x r)
case inr
F : Type ?u.119922
α : Type ?u.119925
β : Type ?u.119928
𝕜 : Type ?u.119931
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ AddSalemSpencer (sphere x r)
convert addSalemSpencer_frontier isClosed_ball (strictConvex_closedBall ℝ x r)
no goals
case h.e'_3
F : Type ?u.119922
α : Type ?u.119925
β : Type ?u.119928
𝕜 : Type ?u.119931
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ sphere x r = frontier (closedBall x r)
exact (frontier_closedBall _ hr).symm