English
If f is a Mul-Freiman isomorphism, then ThreeGPFree(A) iff ThreeGPFree(f[A]).
Русский
Если f — тождественная мультипликативная Фрейман-омография, то A 3GPFree тогда и только тогда, когда образ f(A) 3GPFree.
LaTeX
$$$$ \\text{ThreeGPFree}(f''A) \\iff \\text{ThreeGPFree}(A). $$$$
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 of_image (hf : IsMulFreimanHom 2 s t f) (hf' : s.InjOn f) (hAs : A ⊆ s) (hA : ThreeGPFree (f '' A)) :
ThreeGPFree A := fun _ ha _ hb _ hc habc ↦
hf' (hAs ha) (hAs hb) <|
hA (mem_image_of_mem _ ha) (mem_image_of_mem _ hb) (mem_image_of_mem _ hc) <|
hf.mul_eq_mul (hAs ha) (hAs hc) (hAs hb) (hAs hb) habc
