Graph theory def: Edge connectivity number

[SnirBroshi]

We have SimpleGraph.IsEdgeConnected and SimpleGraph.IsEdgeReachable for edge connectivity of simple graphs.

I suggest we're missing the following definitions:

noncomputable def edgeReachability (G : SimpleGraph V) (u v : V) : ℕ∞ :=
    ⨆ (k : ℕ∞) (_ : G.IsVertexReachable k u v), k

noncomputable def edgeConnectivity (G : SimpleGraph V) (u v : V) : ℕ∞ :=
    ⨆ (k : ℕ∞) (_ : G.IsVertexConnected k), k

and basic API for them.

[SproutSeeds]

Hi! Thanks for opening this issue — I’d be happy to work on it. If that sounds good, I’ll start by introducing edgeReachability and edgeConnectivity with a small initial API in the existing edge-connectivity file, then follow up with any refinements from review.

[SproutSeeds]

Quick update: I opened #36050 with initial definitions for edge reachability and edge connectivity numbers, plus basic comparison lemmas. Happy to adjust naming or API shape based on feedback.