feat:(Combinatorics/SimpleGraph): connected SimpleGraph forms a MetricSpace

[Rida-Hamadani]

---

• depends on: [Merged by Bors] - feat(Combinatorics/SimpleGraph): define edist and rewrite dist #14582

[github-actions]

PR summary a9f18ca4e7

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Metric	523	870	+347 (+66.35%)

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.SimpleGraph.Metric	347

---

Declarations diff

+ Connected.exists_walk_length_eq_dist
+ Connected.exists_walk_length_eq_edist
+ Reachable.exists_walk_length_eq_dist
+ Reachable.exists_walk_length_eq_edist
+ Walk.edist_le
+ dist_eq_sInf
+ edist
+ edist_comm
+ edist_eq_one_iff_adj
+ edist_eq_sInf
+ edist_eq_top_of_not_reachable
+ edist_eq_zero_iff
+ edist_le
+ edist_ne_top_iff_reachable
+ edist_pos_of_ne
+ edist_self
+ edist_triangle
+ exists_walk_of_edist_eq_coe
+ exists_walk_of_edist_ne_top
+ iInf_eq_top_of_isEmpty
+ iInf_eq_zero
+ iInf_toNat
+ instance (h : Connected G) : MetricSpace V
+ reachable_of_edist_ne_top
+ reverse_bijective
+ reverse_injective
+ reverse_surjective
- Connected.exists_walk_of_dist
- Reachable.exists_walk_of_dist

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Combinatorics/SimpleGraph): define edist and rewrite dist #14582
  By Dependent Issues (🤖). Happy coding!

[kmill]

I don't think this is a good idea. I know I suggested it, but I don't think it should be included in mathlib. The problem is that now Verts G is another way to refer to the vertex type, which will create issues.

We should build a bridge to Quiver if we really want this.

[Rida-Hamadani]

Thanks for the review! I will convert this to a draft and work on it.