Theorem SimpleGraph.Subgraph.IsMatching.mem_coe_toEdge

Modification history

2026-05-18 22:44

Mathlib/Combinatorics/SimpleGraph/Matching.lean

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

Added SimpleGraph.Subgraph.IsMatching.mem_coe_toEdge View on Github →