of_image — Mathlib

English

If hf is a Freiman isomorphism and hf' is injective on s, and A ⊆ s × s with IsCornerFree of Prod.map f f '' A, then IsCornerFree A.

Русский

Если hf — изоморфизм Фримана, hf' инъективно на s, A ⊆ s × s и IsCornerFree(Prod.map f f '' A), тогда IsCornerFree A.

LaTeX

$$$ IsCornerFree(Prod.map f f '' A) \Rightarrow IsCornerFree A $$$

Lean4

/-- Corners are preserved under `2`-Freiman homomorphisms. -/
theorem of_image (hf : IsAddFreimanHom 2 s t f) (hf' : s.InjOn f) (hAs : (A : Set (G × G)) ⊆ s ×ˢ s)
    (hA : IsCornerFree (Prod.map f f '' A)) : IsCornerFree A := fun _x₁ _y₁ _x₂ _y₂ hxy ↦
  hf' (hAs hxy.fst_fst_mem).1 (hAs hxy.snd_fst_mem).1 <| hA <| hxy.image hf hAs

Похожие утверждения