Theorem SimpleGraph.edist_bot

Modification history

2024-08-07 16:11
Mathlib/Combinatorics/SimpleGraph/Metric.lean
feat(Combinatorics/SimpleGraph): `dist_bot` and `dist_top` (#15465)
Added SimpleGraph.edist_botView on Github →