Theorems · Theorem · combinatorics

SimpleGraph.Subgraph.IsPerfectMatching.exists_of_isClique_supp

∀ {V : Type u_1} {G : SimpleGraph V} [Finite V],
  Even (Nat.card V) →
    ¬G.IsTutteViolator G.universalVerts →
      (∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp) →
        ∃ M, M.IsPerfectMatching

If the universal vertices of a graph G decompose G into cliques such that the Tutte isn't violated, then G has a perfect matching.

Defined in

Mathlib.Combinatorics.SimpleGraph.Tutte

Cited by

1 results in Mathlib

Foundations

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

Assumes

Finite