Graph theory def: Vertex connectivity

[SnirBroshi]

Vertex connectivity for simple graphs.

I suggest we're missing the following definitions:

def IsVertexReachable (G : SimpleGraph V) (k : ℕ∞) (u v : V) : Prop :=
  -- `G'.Reachable u v` for every graph `G'` which is produced
  -- by removing less than `k` other vertices from `G`

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

def IsVertexPreconnected (G : SimpleGraph V) : Prop :=
  ∀ u v, G.IsVertexReachable k u v

def IsVertexConnected (G : SimpleGraph V) : Prop :=
  k + 1 ≤ ENat.card V ∧ G.IsVertexPreconnected

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

and basic API for them.

[SnirBroshi]

#33355 handles some of these