Commit 2024-04-17 15:12 2e8aeee4

View on Github →

feat(Combinatorics/SimpleGraph): Existence of a path from u to v of length equal to G.dist u v (#11814) Checkout this conversation on zulip.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

added theorem SimpleGraph.Walk.bypass_eq_self_of_length_le

Modified Mathlib/Combinatorics/SimpleGraph/Metric.lean

added theorem SimpleGraph.Connected.exists_path_of_dist

added theorem SimpleGraph.Reachable.exists_path_of_dist

added theorem SimpleGraph.Walk.isPath_of_length_eq_dist