exists_maximal_isMatchingFree — Mathlib

English

For a finite graph, if M is a perfect matching, then the vertex count is even.

Русский

Для конечного графа, если есть совершенное совпадение M, то количество вершин чётно.

LaTeX

$$Even(Fintype.card V)$$

Lean4

theorem exists_maximal_isMatchingFree [Finite V] (h : G.IsMatchingFree) :
    ∃ Gmax : SimpleGraph V, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G', G' > Gmax → ∃ M : Subgraph G', M.IsPerfectMatching :=
  by
  simp_rw [← @not_forall_not _ Subgraph.IsPerfectMatching]
  obtain ⟨Gmax, hGmax⟩ := Finite.exists_le_maximal h
  exact ⟨Gmax, ⟨hGmax.1, ⟨hGmax.2.prop, fun _ h' ↦ hGmax.2.not_prop_of_gt h'⟩⟩⟩

Похожие утверждения