English
Geometric progressions of length three are preserved under semigroup homomorphisms: if f is a homomorphism and the image of s is GP-free, then the image of s is GP-free (and conversely under the right hypotheses).
Русский
Геометрические прогрессии длины три сохраняются под полугомоморфизмами: если f — полугомоморфизм и образ s GP-free, то образ s GP-free (и наоборот при подходящих условиях).
LaTeX
$$$[FunLike\ F\alpha\beta]\ [MulHomClass\ F\alpha\beta]\; (f : F) \land InjOn((s \cdot s), f) \Rightarrow (ThreeGPFree s) \Rightarrow ThreeGPFree(f''s)$$$
Lean4
/-- Geometric progressions of length three are preserved under semigroup homomorphisms. -/
@[to_additive /-- Arithmetic progressions of length three are preserved under semigroup homomorphisms. -/
]
theorem image' [FunLike F α β] [MulHomClass F α β] (f : F) (hf : (s * s).InjOn f) (h : ThreeGPFree s) :
ThreeGPFree (f '' s) := by
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ habc
rw [h ha hb hc (hf (mul_mem_mul ha hc) (mul_mem_mul hb hb) <| by rwa [map_mul, map_mul])]
