Theorems · Definition · combinatorics

SimpleGraph.CompleteEquipartiteSubgraph.mk.noConfusion

{V : Type u_1} →
  {G : SimpleGraph V} →
    {r t : ℕ} →
      {P : Sort u} →
        {parts : Finset (Finset V)} →
          {card_parts : parts.card = r ∨ t = 0} →
            {card_mem_parts : ∀ {p : Finset V}, p ∈ parts → p.card = t} →
              {isCompleteBetween : (↑parts).Pairwise fun x1 x2 => G.IsCompleteBetween ↑x1 ↑x2} →
                {parts' : Finset (Finset V)} →
                  {card_parts' : parts'.card = r ∨ t = 0} →
                    {card_mem_parts' : ∀ {p : Finset V}, p ∈ parts' → p.card = t} →
                      {isCompleteBetween' : (↑parts').Pairwise fun x1 x2 => G.IsCompleteBetween ↑x1 ↑x2} →
                        { parts := parts, card_parts := card_parts, card_mem_parts := card_mem_parts,
                              isCompleteBetween := isCompleteBetween } =
                            { parts := parts', card_parts := card_parts', card_mem_parts := card_mem_parts',
                              isCompleteBetween := isCompleteBetween' } →
                          (parts ≍ parts' → P) → P

Defined in

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Cited by

1 results in Mathlib

Foundations

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