Theorem SimpleGraph.Subgraph.IsMatching.injOn_edgeSet

Modification history

2026-07-17 09:57

Mathlib/Combinatorics/SimpleGraph/Matching.lean

chore(Data): rename `setOf` to `Set.ofPred` (#41507) …

Modified SimpleGraph.Subgraph.IsMatching.injOn_edgeSet View on Github →

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.injOn_edgeSet View on Github →