Theorems · Theorem · combinatorics

SimpleGraph.exists_isTutteViolator

∀ {V : Type u_1} {G : SimpleGraph V} [Finite V],
  (∀ (M : G.Subgraph), ¬M.IsPerfectMatching) → Even (Nat.card V) → ∃ u, G.IsTutteViolator u

From a graph on an even number of vertices with no perfect matching, we can remove an odd number of vertices such that there are more odd components in the resulting graph than vertices we removed. This is the sufficiency side of Tutte's theorem.

Defined in

Mathlib.Combinatorics.SimpleGraph.Tutte

Cited by

1 results in Mathlib

Foundations

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

Assumes

Finite