Theorems · Theorem · combinatorics

SimpleGraph.CompleteEquipartiteSubgraph.mk.inj

∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} {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_1 : Finset (Finset V)}
  {card_parts_1 : parts_1.card = r ∨ t = 0} {card_mem_parts_1 : ∀ {p : Finset V}, p ∈ parts_1 → p.card = t}
  {isCompleteBetween_1 : (↑parts_1).Pairwise fun x1 x2 => G.IsCompleteBetween ↑x1 ↑x2},
  { parts := parts, card_parts := card_parts, card_mem_parts := card_mem_parts,
        isCompleteBetween := isCompleteBetween } =
      { parts := parts_1, card_parts := card_parts_1, card_mem_parts := card_mem_parts_1,
        isCompleteBetween := isCompleteBetween_1 } →
    parts = parts_1

Defined in

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Cited by

1 results in Mathlib

Foundations

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