graph_matching_num_bot
theoremverified
The matching number of the empty graph (bot) is 0.
Statement
theorem graph_matching_num_bot {V : Type*} : graph_matching_num (⊥ : SimpleGraph V) = 0
- Verified
- 06 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.
Lean source view module on GitHub
/-- The empty graph has matching number 0. -/ theorem graph_matching_num_bot {V : Type*} : graph_matching_num (⊥ : SimpleGraph V) = 0 := by unfold graph_matching_num apply le_antisymm · refine iSup_le fun M => iSup_le fun _ => ?_ have h : M.edgeSet = ∅ := Set.subset_empty_iff.mp (SimpleGraph.edgeSet_bot ▸ M.edgeSet_subset) rw [h, Set.encard_empty] · exact zero_le