English
If a graph has a clique-supplementation structure as in Tutte, then there exists a perfect matching.
Русский
Если граф обладает структурой clique-supp как в Тутте, то существует совершенное совпадение.
LaTeX
$$∃ M ⊆ G, M.IsPerfectMatching$$
Lean4
/-- 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. -/
theorem exists_of_isClique_supp (hveven : Even (Nat.card V)) (h : ¬G.IsTutteViolator G.universalVerts)
(h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp) :
∃ (M : Subgraph G), M.IsPerfectMatching := by
classical
cases nonempty_fintype V
obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
obtain ⟨M', hM'⟩ :=
((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching (Set.toFinite _)).mp
(by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card, ← Set.ncard_eq_toFinset_card'] using hM.even_card)
refine ⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩
· simp [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, disjoint_compl_right]
· rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
exact M.verts.union_compl_self
