simple graph connectivity question

Stream: mathlib4

[Chen Ling]

I'm reading SimpleGraph APIs, and I find when saying G : SimpleGraph V, we mean G has some vertices and edges, but V can be arbitrary something?
And to say G.connected iff ..., must I prove the whole V has some good properties? If I only have something to say about edges set and vertices set of G, maybe I can only say G.support is connected or something like this?
Have I got anything wrong?

[Ilmārs Cīrulis]

Here is how SImpleGraph is defined:

/-- A simple graph is an irreflexive symmetric relation Adj on a vertex type V.
The relation describes which pairs of vertices are adjacent.
There is exactly one edge for every pair of adjacent vertices;
see SimpleGraph.edgeSet for the corresponding edge set.
-/
@[ext, aesop safe constructors (rule_sets := [SimpleGraph])]
structure SimpleGraph (V : Type u) where
/-- The adjacency relation of a simple graph. -/
Adj : V → V → Prop
symm : Symmetric Adj := by aesop_graph
loopless : Irreflexive Adj := by aesop_graph

As one can see the V is just a type of vertices, the "main" part is the adjacency relation Adj with two properties it has to satisfy.

About support... The vertices can be "lonely" or without any edges incident to them. In such case they are still part of the graph , but not part of graph's support.

[Chen Ling]

I see, so a graph G may have some "lonely" vertices without edges. Support is not the vertices set, but those with edges. And we can distinguish a graph is connected, and all edges of a graph is in a connect component.

[Jakub Nowak]

SimpleGraph.Connected is defined such that every vertex has to be connected, not just vertices from SimpleGraph.support. In fact support of connected graph has to be entire V: SimpleGraph.Preconnected.support_eq_univ, i.e. it has no "lonely" vertices.

[Snir Broshi]

btw the common term for "lonely" is isolated vertex