English
If f is a 2-Freiman isomorphism between s and t, and A ⊆ s × s, then corner-structure is preserved under the image map: IsCorner (Prod.map f f '' A) (f x1) (f y1) (f x2) (f y2) ↔ IsCorner A x1 y1 x2 y2.
Русский
Если f является 2‑Freiman изоморфизмом между s и t, и 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(\mathrm{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
/-- A **corner-free set** in an abelian group is a set containing no non-trivial corner. -/
def IsCornerFree (A : Set (G × G)) : Prop :=
∀ ⦃x₁ y₁ x₂ y₂⦄, IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂
