graph_matching_num_mono

theoremverified

If 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'.

Statement

theorem graph_matching_num_mono {V : Type*} {G G' : SimpleGraph V} (h : G ≤ G') :
    graph_matching_num G ≤ graph_matching_num G'

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 two simple graphs G and G' on V, if G ≤ G' (i.e., every edge of G is an edge of G'), then graph_matching_num G ≤ graph_matching_num G'.

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 subgraph is at most that of the supergraph. -/
theorem graph_matching_num_mono {V : Type*} {G G' : SimpleGraph V} (h : G ≤ G') :
    graph_matching_num G ≤ graph_matching_num G' := by
  unfold graph_matching_num
  refine iSup_le fun M => iSup_le fun hM => ?_
  have hM' : (M.map (SimpleGraph.Hom.ofLE h)).IsMatching := hM.map_ofLE h
  have hedge : (M.map (SimpleGraph.Hom.ofLE h)).edgeSet = M.edgeSet := by
    rw [SimpleGraph.Subgraph.edgeSet_map]
    have : (Sym2.map (SimpleGraph.Hom.ofLE h : V → V) : Sym2 V → Sym2 V) = id := by ext ⟨a, b⟩; rfl
    rw [this, Set.image_id]
  rw [← hedge]
  exact le_iSup_of_le (M.map (SimpleGraph.Hom.ofLE h)) (le_iSup_of_le hM' le_rfl)

Discuss this result Challenge it