feat: simple undirected graph definitions

[sorrachai]

This PR introduces the foundational graph definitions for CSLib, including Edge, SimpleGraph, IncidentEdgeSet, Neighbors, and subgraphOf.

Motivation The graph definitions in this file intentionally diverge from those in Mathlib; we prioritise representations that support algorithmic reasoning over those designed for classical combinatorial arguments. In particular, the use of Finset throughout — rather than decidable predicates — makes definitions more directly computable and better suited for verified algorithms.

Main definitions
Edge — undirected edge as an unordered pair via Sym2
SimpleGraph — finite, loopless, simple graph structure
IncidentEdgeSet — edges incident to a given vertex
Neighbors — open neighbourhood of a given vertex
subgraphOf — subgraph relation on SimpleGraph

Future work
We plan to add more fundamental graph algorithms that build on top of this definition.

[Shreyas4991]

The design and purpose of this PR needs substantial Zulip discusssion.

Pros:

It adds vertex sets to simple graph. A longstanding demand of mine which I am implementing for digraphs. I am glad that this issue is being addressed here. This means we can do away with the duplication introduced by a separate subgraph type.

Cons:

The other claims are far from clear. All features algorithmists need from SimpleGraph can be deduced from the mathlib API already. For instance getting the neighborFinset is a trivial step. One just needs the decidable declarations on top of one's file.
This PR will have to reinvent several thousand lines of mathlib API and they will be largely duplicate. Further this will also duplicate Peter Nelson's Graph API that's being built up in mathlib.

My recommendation:

Please discuss in Zulip first. It might be worth a few mathlib PRs to add vertex sets to SimpleGraph. But that is better than carrying this parallel copy without a consensus in the community.

Extra suggestion : if you find the existing API inconvenient then it is a sign of missing simp or grind lemmas. It can make sense to have a math folder where we place this lemmas before upstreaming. This PR could instead provide the interface lemmas. Of course adding vertex sets will require a mathlib PR.

[Shreyas4991]

You don't want to put Finset here. Set is enough, followed by finite instances. There are instances in CS theory where we do actually deal with arbitrary sets of edges without using finiteness. Just not in algorithms.

[sorrachai]

The focus here is on graph algorithms, which by default require finite graphs. Those with infinite graphs should use the definition from Mathlib instead.

[Shreyas4991]

That's not my point. Getting finite graphs from mathlib is trivial. Replicating and maintaining compatible API with mathlib is complex. For most operations you perform with Finsets you only need Sets.

Where you need finiteness, it suffices to put Finite and Fintype instances.

[Shreyas4991]

Same as above. For SimpleGraph, it suffices to have the edge prop as in mathlib. Then neighborFinset can be used with LocallyFinite typeclass. This can further be converted to lists if desired.

[Shreyas4991]

In this case again I think it is better to adapt IsSubgraph. Concretely because all the order theory already exists for this (and it matters even in algorithms where we use them implicitly).

[Shreyas4991]

Continuing the above, you should in all likelihood introduce the relevant order theory instances. See mathlib4#33466 for an example of graphs with vertex sets getting order theory instances. The notation for subgraphs follows from that.