Theorems · Theorem · combinatorics

IsCornerFree.of_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},
  IsAddFreimanHom 2 s t f → Set.InjOn f s → A ⊆ s ×ˢ s → IsCornerFree (Prod.map f f '' A) → IsCornerFree A

Corners are preserved under 2-Freiman homomorphisms.

Defined in

Mathlib.Combinatorics.Additive.Corner.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoid