English
Let s ⊆ α and t ⊆ β be subsets of commutative monoids, and let f: α → β be a map that is a 2-Freiman homomorphism from s to t and injective on s. If t has no geometric progression of length three, then s has no geometric progression of length three.
Русский
Пусть s ⊆ α и t ⊆ β — подмножества коммутативных моидов, и пусть f: α → β удовлетворяет условию 2-Freiman-гомоморфизма от s в t и инъективности на s. Если t не содержит геометрических прогрессий длины три, то и в s их нет.
LaTeX
$$$IsMulFreimanHom(2, s, t, f) \land InjOn(f, s) \land ThreeGPFree(t) \Rightarrow ThreeGPFree(s)$$$
Lean4
/-- Geometric progressions of length three are reflected under `2`-Freiman homomorphisms. -/
@[to_additive /-- Arithmetic progressions of length three are reflected under `2`-Freiman homomorphisms. -/
]
theorem threeGPFree (hf : IsMulFreimanHom 2 s t f) (hf' : s.InjOn f) (ht : ThreeGPFree t) : ThreeGPFree s :=
(ht.mono hf.mapsTo.image_subset).of_image hf hf' subset_rfl
