English
Corners are preserved under 2-Freiman homomorphisms: If hf is an IsAddFreimanIso and A ⊆ s × s, then IsCorner (Prod.map f f '' A) (f x1) (f y1) (f x2) (f y2) holds iff IsCorner A x1 y1 x2 y2 holds.
Русский
Углы сохраняются под 2‑Freiman гомоморфизмами: если hf есть IsAddFreimanIso и A ⊆ s × s, то IsCorner (Prod.map f f '' A) (f x1) (f y1) (f x2) (f y2) эквивалентно IsCorner A x1 y1 x2 y2.
LaTeX
$$$ IsCorner (Prod.map f f '' A) (f x_1) (f y_1) (f x_2) (f y_2) \iff IsCorner A x_1 y_1 x_2 y_2 $$$
Lean4
/-- Corners are preserved under `2`-Freiman homomorphisms. -/
theorem image (hf : IsAddFreimanHom 2 s t f) (hAs : (A : Set (G × G)) ⊆ s ×ˢ s) (hA : IsCorner A x₁ y₁ x₂ y₂) :
IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) :=
by
obtain ⟨hx₁y₁, hx₁y₂, hx₂y₁, hxy⟩ := hA
exact
⟨mem_image_of_mem _ hx₁y₁, mem_image_of_mem _ hx₁y₂, mem_image_of_mem _ hx₂y₁,
hf.add_eq_add (hAs hx₁y₁).1 (hAs hx₁y₂).2 (hAs hx₂y₁).1 (hAs hx₁y₁).2 hxy⟩
