Theorem SimpleGraph.edist_bot_of_ne

Modification history

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