English
Additive three-term progression-free property has a right-side cancellation characterization: ThreeAPFree s is equivalent to the right-cancellation condition a + c = b + b → b = c for all a,b,c in s.
Русский
Свойство трехчленного AP-free для множества имеет правую характеристику отмены: ThreeAPFree s эквивалентно условию a + c = b + b → b = c для всех a,b,c ∈ s.
LaTeX
$$$ThreeAPFree\ s \iff \forall a\in s\forall b\in s\forall c\in s, a+c=b+b \Rightarrow a=c$$$
Lean4
theorem threeAPFree_iff_eq_right {s : Set ℕ} :
ThreeAPFree s ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → ∀ ⦃c⦄, c ∈ s → a + c = b + b → a = c :=
by
refine forall₄_congr fun a _ha b hb => forall₃_congr fun c hc habc => ⟨?_, ?_⟩
· rintro rfl
exact (add_left_cancel habc).symm
· rintro rfl
simp_rw [← two_mul] at habc
exact mul_left_cancel₀ two_ne_zero habc
