English
Same as previous: 3GPFree is preserved under 2-Freiman isomorphisms.
Русский
Та же идея: 3GPFree сохраняется под 2-Freiman изоморфизмами.
LaTeX
$$$$ \\text{ThreeGPFree}(f''A) \\iff \\text{ThreeGPFree}(A). $$$$
Lean4
/-- Geometric progressions of length three are unchanged under `2`-Freiman isomorphisms. -/
@[to_additive /-- Arithmetic progressions of length three are unchanged under `2`-Freiman isomorphisms. -/
]
theorem threeGPFree_image (hf : IsMulFreimanIso 2 s t f) (hAs : A ⊆ s) : ThreeGPFree (f '' A) ↔ ThreeGPFree A :=
by
rw [ThreeGPFree, ThreeGPFree]
have := (hf.bijOn.injOn.mono hAs).bijOn_image (f := f)
simp +contextual only [((hf.bijOn.injOn.mono hAs).bijOn_image (f := f)).forall,
hf.mul_eq_mul (hAs _) (hAs _) (hAs _) (hAs _), this.injOn.eq_iff]
