English
Let f be an additive Freiman 2-iso between two Abelian groups, and let A be a subset of s × s. Then the set obtained by applying the product map f to each coordinate, Prod.map f f '' A, is corner-free if and only if A is corner-free.
Русский
Пусть f — добавительно-Фримановская изоморфия порядка 2 между двумя абелными группами, а A ⊆ s × s. Тогда множество Prod.map f f '' A сохраняет свойство свободности от углов: оно является углово-свободным тогда и только тогда, когда A углово-свободна.
LaTeX
$$$IsCornerFree\bigl(\mathrm{Prod.map}\ f\ f\ ''\ A\bigr) \iff IsCornerFree(A),$ при условии $IsAddFreimanIso\ 2\ s\ t\ f$ и $A \subseteq s \times s$.$$
Lean4
theorem isCornerFree_image (hf : IsAddFreimanIso 2 s t f) (hAs : A ⊆ s ×ˢ s) :
IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A :=
by
have : Prod.map f f '' A ⊆ t ×ˢ t := ((hf.bijOn.mapsTo.prodMap hf.bijOn.mapsTo).mono hAs Subset.rfl).image_subset
rw [isCornerFree_iff hAs, isCornerFree_iff this]
simp +contextual only [hf.bijOn.forall, isCorner_image hf hAs, hf.bijOn.injOn.eq_iff]
