Theorems · Theorem · combinatorics

isCornerFree_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}, IsAddFreimanIso 2 s t f → A ⊆ s ×ˢ s → (IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A)

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