graph_matching_num_le_encard_edgeSet
theoremverified
In any simple graph G, the matching number is at most the cardinality of the edge set.
Statement
theorem graph_matching_num_le_encard_edgeSet {V : Type*} (G : SimpleGraph V) : graph_matching_num G ≤ G.edgeSet.encard
- Source
- folklore
- Verified
- 07 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 1
- graph_matching_numThe matching number of a graph G is the supremum of the cardinalities of the edge sets of all matchings in G.
Read back from the Lean
For any type V and any simple graph G on V, the matching number of G (defined as graph_matching_num G) is less than or equal to the extended cardinality (encard) of the edge set of G (in ℕ∞).
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- The matching number of a simple graph is at most the cardinality of its edge set. -/ theorem graph_matching_num_le_encard_edgeSet {V : Type*} (G : SimpleGraph V) : graph_matching_num G ≤ G.edgeSet.encard := by unfold graph_matching_num exact iSup_le fun M => iSup_le fun _ => Set.encard_le_encard M.edgeSet_subset