English
A sphere in a normed space is ThreeAPFree; more precisely, the set of points at distance r from a center x is three-AP free when r > 0, with the singleton case handled separately.
Русский
Сфера в нормированном пространстве не содержит ненулевых арифметических прогрессий из трех членов; для r > 0 следует, что сфера ThreeAPFree.
LaTeX
$$$$ ThreeAPFree(\mathrm{sphere}(x,r)) $$$$
Lean4
theorem threeAPFree_sphere {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] (x : E)
(r : ℝ) : ThreeAPFree (sphere x r) := by
obtain rfl | hr := eq_or_ne r 0
· rw [sphere_zero]
exact threeAPFree_singleton _
· convert threeAPFree_frontier isClosed_closedBall (strictConvex_closedBall ℝ x r)
exact (frontier_closedBall _ hr).symm
