Theorem SimpleGraph.Subgraph.edgeSet_monotone

Modification history

2026-05-18 22:44
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
feat(Combinatorics/SimpleGraph/Matching): `edgeSet` is injective and strictly monotonic on matchings, and more API (#36451)
Added SimpleGraph.Subgraph.edgeSet_monotoneView on Github →