feat(Combinatorics/Graph): connected graphs

[Jun2M]

This PR introduces

• IsConnectedComponentOf, a graph is a connected component of another graph, and
• IsConnected, a graph is a self component

Under this definition, an empty graph is not connected.

Co-authored-by: Peter Nelson apn.uni@gmail.com

---

• depends on: [Merged by Bors] - feat(Combinatorics/Graph): OrderBot instance for Graph #37610
• depends on: feat(Combinatorics/GraphLike): introduce GraphLike typeclass #36743

[github-actions]

PR summary 2a556ee342

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.Graph.Connected.Component (new file)	494

---

Declarations diff

+ Connected
+ Connected.exists_inc_notMem_of_lt
+ Connected.ext_of_isClosedSubgraph
+ Connected.nonempty
+ IsConnectedComponentOf
+ IsConnectedComponentOf.Connected
+ anti_right
+ connected_iff_forall_closed
+ connected_iff_forall_closed_ge
+ isClosedSubgraph
+ isInducedSubgraph
+ le
+ nonempty
+ not_connected_bot

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(Combinatorics/Graph): OrderBot instance for Graph #37610
• feat(Combinatorics/GraphLike): introduce GraphLike typeclass #36743
  By Dependent Issues (🤖). Happy coding!

[YaelDillies]

What's the plan for IsPreconnected? Will you define it later as "for all u, v, u is reachable from v"?

[Jun2M]

@YaelDillies, that is exactly the definition of IsPreconnected we have in the Matroid repo. However, Walk is still held up by GraphLike. (although it is almost there! I think we have something everyone is happy with and I just need to put it into Lean) One way is to wait for that.

Alternative, thanks to Menger, is ∀ S ⊆ V(G), δ(G, S) = ∅ ↔ S = ∅ ∨ S = V(G) using δ(G, S) defined in #37865.

[YaelDillies]

It is difficult to evaluate Connected without Preconnected: is it easy to go from one to the other? Will they live in the same file? What about Reachable? etc...