Mathlib Map

Theorems · Theorem · combinatorics

IsCorner.fst_fst_mem

∀ {G : Type u_1} [inst : AddCommMonoid G] {A : Set (G × G)} {x₁ y₁ x₂ y₂ : G}, IsCorner A x₁ y₁ x₂ y₂ → (x₁, y₁) ∈ A
Defined in
Mathlib.Combinatorics.Additive.Corner.Defs
Cited by
4 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
AddCommMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Set.Subsingleton.isCornerFree · cited by 2Subsingleton.isCornerFreeIsCornerFree.of_image · cited by 1IsCornerFree.of_imageisCornerFree_iff · cited by 1isCornerFree_iffIsCorner.mono · cited by 1IsCorner.monoSet · cited by 53352SetAddCommMonoid · cited by 12281AddCommMonoidIsCorner · cited by 16IsCornerIsCorner.fst_fst_memCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • AddCommMonoidstatement and proof · cited by 12,281
  • IsCornerstatement and proof · cited by 16

Cited by4

Results whose statement or proof uses this declaration.