Theorems · Theorem · combinatorics

SimpleGraph.completeEquipartiteGraph_succ_isContained_iff

∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ},
  (SimpleGraph.completeEquipartiteGraph (r + 1) t).IsContained G ↔
    ∃ K s, s.card = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s

Simple graphs contain a copy of a completeEquipartiteGraph (r + 1) t iff there exists s : Finset V of size #s = t and K : G.CompleteEquipartiteSubgraph r t such that the vertices in s are adjacent to the vertices in K.

Defined in

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Cited by

0 results in Mathlib

Foundations

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