feat(Combinatorics/SimpleGraph/Path): ConnectedComponent.toSubgraph

[LeoDog896]

This introduces ConnectedComponent.toSubgraph, and proves that connected components are connected.

---

[github-actions]

PR summary 78fa4d94de

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ induce_induce
+ induce_top_verts
+ instance (p : G.Walk u v) (h : w ∈ p.support) : CoeDep V w p.toSubgraph.verts
+ instance (p : G.Walk u v) : CoeDep V u p.toSubgraph.verts
+ instance (p : G.Walk u v) : CoeDep V v p.toSubgraph.verts
+ subgraph_mapLe
+ supp_nonEmpty
+ supp_verts_mk_eq
+ toSubgraph
+ toSubgraph_coe_connected
+ toSubgraph_coe_walk
+ toSubgraph_connected
+ toSubgraph_nil_singleton
+ toSubgraph_reachable
+ toSubgraph_subgraph_coe_walk
+ toSubgraph_support
+ toSubgraph_vertices

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).