graph_matching_num
def
The matching number of a graph G is the supremum of the cardinalities of the edge sets of all matchings in G.
Statement
noncomputable def graph_matching_num {V : Type*} (G : SimpleGraph V) : ℕ∞
- Verified
- 06 Sep 2026
- Axioms
- none listed
- Used by 5
- 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.
- graph_matching_num_le_encard_edgeSetIn any simple graph G, the matching number is at most the cardinality of the edge set.
- graph_matching_num_monoIf G and G' are simple graphs on the same vertex set with G ≤ G', then the matching number of G is at most the matching number of G'.
- graph_matching_num_le_vertex_cover_numIn any simple graph G, the matching number is at most the vertex cover number.
- graph_matching_num_botThe matching number of the empty graph (bot) is 0.
Lean source view module on GitHub
/-- The matching number of a graph, defined as the supremum of cardinalities of edge sets of matchings in G. -/ noncomputable def graph_matching_num {V : Type*} (G : SimpleGraph V) : ℕ∞ := ⨆ (M : SimpleGraph.Subgraph G) (_ : M.IsMatching), M.edgeSet.encard