Commit 2024-08-07 16:11 2da5149f

View on Github →

feat(Combinatorics/SimpleGraph): dist_bot and dist_top (#15465)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Metric.lean

added theorem SimpleGraph.dist_bot

added theorem SimpleGraph.dist_top

added theorem SimpleGraph.dist_top_of_ne

added theorem SimpleGraph.edist_bot

added theorem SimpleGraph.edist_bot_of_ne

added theorem SimpleGraph.edist_top

added theorem SimpleGraph.edist_top_of_ne

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.reachable_bot