Theorems · Theorem · combinatorics

IsCorner.image

∀ {G : Type u_1} {H : Type u_2} [inst : AddCommMonoid G] [inst_1 : AddCommMonoid H] {A : Set (G × G)} {s : Set G}
  {t : Set H} {f : G → H} {x₁ y₁ x₂ y₂ : G},
  IsAddFreimanHom 2 s t f →
    A ⊆ s ×ˢ s → IsCorner A x₁ y₁ x₂ y₂ → IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)

Corners are preserved under 2-Freiman homomorphisms.

Defined in

Mathlib.Combinatorics.Additive.Corner.Defs

Cited by

1 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

AddCommMonoidAddCommMonoid