Commit 2026-05-18 22:44 25a090d3

View on Github →

feat(Combinatorics/SimpleGraph/Matching): edgeSet is injective and strictly monotonic on matchings, and more API (#36451)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

added theorem SimpleGraph.Subgraph.IsMatching.injOn_edgeSet

added theorem SimpleGraph.Subgraph.IsMatching.mem_coe_toEdge

added theorem SimpleGraph.Subgraph.IsMatching.strictMonoOn_edgeSet

modified theorem SimpleGraph.Subgraph.IsMatching.toEdge_eq_of_adj

modified theorem SimpleGraph.Subgraph.IsMatching.toEdge_eq_toEdge_of_adj

added theorem SimpleGraph.Subgraph.IsMatching.toEdge_preimage_singleton

added theorem SimpleGraph.Subgraph.IsMatching.verts_eq_biUnion_edgeSet

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

added theorem SimpleGraph.Subgraph.edgeSet_monotone