Theorems · Definition · combinatorics

SimpleGraph.IsSRGWith.casesOn

{V : Type u} →
  [inst : Fintype V] →
    {G : SimpleGraph V} →
      [inst_1 : DecidableRel G.Adj] →
        {n k ℓ μ : ℕ} →
          {motive : G.IsSRGWith n k ℓ μ → Sort u_1} →
            (t : G.IsSRGWith n k ℓ μ) →
              ((card : Fintype.card V = n) →
                  (regular : G.IsRegularOfDegree k) →
                    (of_adj : ∀ (v w : V), G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) = ℓ) →
                      (of_not_adj : Pairwise fun v w => ¬G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) = μ) →
                        motive ⋯) →
                motive t

Defined in

Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Cited by

0 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableRel