Mathlib Map

Theorems · Definition · combinatorics

IsCorner.casesOn

{G : Type u_1} →
  [inst : AddCommMonoid G] →
    {A : Set (G × G)} →
      {x₁ y₁ x₂ y₂ : G} →
        {motive : IsCorner A x₁ y₁ x₂ y₂ → Sort u} →
          (t : IsCorner A x₁ y₁ x₂ y₂) →
            ((fst_fst_mem : (x₁, y₁) ∈ A) →
                (fst_snd_mem : (x₁, y₂) ∈ A) →
                  (snd_fst_mem : (x₂, y₁) ∈ A) → (add_eq_add : x₁ + y₂ = x₂ + y₁) → motive ⋯) →
              motive t
Defined in
Mathlib.Combinatorics.Additive.Corner.Defs
Cited by
2 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
AddCommMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

isCorner_iff · cited by 1isCorner_iffIsCorner.image · cited by 1IsCorner.imageSet · cited by 53352SetAddCommMonoid · cited by 12281AddCommMonoidIsCorner · cited by 16IsCornerIsCorner.casesOnCITED 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 by2

Results whose statement or proof uses this declaration.