noncomputable def SimpleGraph.matchingNumber {α : Type u_1} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ

matchingNumber G is the size of a maximum matching of G.

Equations

• G.matchingNumber = sSup ((fun (M : G.Subgraph) => ↑M.edgeSet.toFinset.card) '' {M : G.Subgraph | M.IsMatching})

theorem SimpleGraph.matching_card_bound {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) (M : G.Subgraph) [Fintype ↑M.edgeSet] (h : M.IsMatching) : 2 * M.edgeSet.toFinset.card ≤ Fintype.card α

In a finite graph, twice the number of edges of any matching is at most the number of vertices: each edge contributes two distinct vertices, and a matching's edges are vertex-disjoint.