noncomputable def SimpleGraph.oddComponentCount {V : Type u_1} (G : SimpleGraph V) (X : Set V) : ℕ

theorem SimpleGraph.oddComponentCount_le_ncard_of_isPerfectMatching {V : Type u_1} [Finite V] {G : SimpleGraph V} {M : G.Subgraph} (hM : M.IsPerfectMatching) (X : Set V) : G.oddComponentCount X ≤ X.ncard

theorem SimpleGraph.isPerfectMatching_of_oddComponentCount_le {V : Type u_1} [Finite V] {G : SimpleGraph V} (h : ∀ (X : Set V), G.oddComponentCount X ≤ X.ncard) : ∃ (M : G.Subgraph), M.IsPerfectMatching

theorem SimpleGraph.tutte_theorem {V : Type u_1} [Finite V] {G : SimpleGraph V} : (∃ (M : G.Subgraph), M.IsPerfectMatching) ↔ ∀ (X : Set V), G.oddComponentCount X ≤ X.ncard