English
Geometric progressions of length three are preserved under bijective 2-Freiman isomorphisms: if A and B are in bijection via f and A ≃ B in the Freiman sense, then ThreeGPFree(A) holds exactly when ThreeGPFree(B) holds.
Русский
Геометрические прогрессии длины три сохраняются под биективными 2-Freiman-изоморфизмами: если A и B эквивалентны по фактору Фримана и существует biunivoc f, то свойство GP-free сохраняется: ThreeGPFree(A) равно ThreeGPFree(B).
LaTeX
$$$IsMulFreimanIso(2, s, t, f) \Rightarrow (ThreeGPFree(s) \leftrightarrow ThreeGPFree(t))$$$
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_congr (hf : IsMulFreimanIso 2 s t f) : ThreeGPFree s ↔ ThreeGPFree t := by
rw [← threeGPFree_image hf subset_rfl, hf.bijOn.image_eq]
