threeAPFree_image_sphere — Mathlib

English

The image of Behrend's sphere under the map (2d−1) is three-term arithmetic progression free.

Русский

Образ сферы Behrend под отображением map(2d−1) не содержит троек AP.

LaTeX

$$ThreeAPFree\\big( ((\\text{sphere } n d k).image (map (2 * d - 1))) : Set \\mathbb{N} \\big) $$

Lean4

theorem threeAPFree_image_sphere : ThreeAPFree ((sphere n d k).image (map (2 * d - 1)) : Set ℕ) :=
  by
  rw [coe_image]
  apply
    ThreeAPFree.image' (α := Fin n → ℕ) (β := ℕ) (s := sphere n d k) (map (2 * d - 1)) (map_injOn.mono _)
      threeAPFree_sphere
  rw [Set.add_subset_iff]
  rintro a ha b hb i
  have hai := mem_box.1 (sphere_subset_box ha) i
  have hbi := mem_box.1 (sphere_subset_box hb) i
  rw [lt_tsub_iff_right, ← succ_le_iff, two_mul]
  exact (add_add_add_comm _ _ 1 1).trans_le (_root_.add_le_add hai hbi)

Похожие утверждения