graph_matching_num_le_vertex_cover_num
theoremverified
In any simple graph G, the matching number is at most the vertex cover number.
Statement
theorem graph_matching_num_le_vertex_cover_num {V : Type*} (G : SimpleGraph V) : graph_matching_num G ≤ G.vertexCoverNum
- Verified
- 06 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 2
- graph_matching_numThe matching number of a graph G is the supremum of the cardinalities of the edge sets of all matchings in G.
- graph_matching_encard_le_vertex_cover_encardFor any matching M and any vertex cover c of a simple graph G, the number of edges in M is at most the number of vertices in c.
Lean source view module on GitHub
/-- Weak duality: matching number is bounded above by vertex cover number. -/ theorem graph_matching_num_le_vertex_cover_num {V : Type*} (G : SimpleGraph V) : graph_matching_num G ≤ G.vertexCoverNum := by obtain ⟨s, hs1, hs2⟩ := G.vertexCoverNum_exists exact iSup_le fun M => iSup_le fun hM => hs1 ▸ graph_matching_encard_le_vertex_cover_encard G M s hM hs2