Theorem SimpleGraph.maxDegree_mono

Modification history

2026-04-23 08:52

Mathlib/Combinatorics/SimpleGraph/Copy.lean

feat(Combinatorics/SimpleGraph/Copy): `maxDegree` is monotonic, and `minDegree` is monotonic over a surjective `Copy` (#38355)

Added SimpleGraph.maxDegree_mono View on Github →