English
The Behrend sphere, viewed as a set, is three-term arithmetic progression free.
Русский
Сфера Behrend, рассматриваемая как множество, не содержит тройки в арифметической прогрессии.
LaTeX
$$$ ThreeAPFree\\big(\\text{sphere}(n,d,k).toSet\\big) $$$
Lean4
nonrec theorem threeAPFree_sphere : ThreeAPFree (sphere n d k : Set (Fin n → ℕ)) :=
by
set f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
{ toFun := fun f => ((↑) : ℕ → ℝ) ∘ f
map_zero' := funext fun _ => cast_zero
map_add' := fun _ _ => funext fun _ => cast_add _ _ }
refine
ThreeAPFree.of_image (AddMonoidHomClass.isAddFreimanHom f (Set.mapsTo_image _ _)) cast_injective.comp_left.injOn
(Set.subset_univ _) ?_
refine (threeAPFree_sphere 0 (√↑k)).mono (Set.image_subset_iff.2 fun x => ?_)
rw [Set.mem_preimage, mem_sphere_zero_iff_norm]
exact norm_of_mem_sphere
