Conventions for graph defs

Stream: general

[Aaron Anderson]

While working on #3458, @Kyle Miller and I had a lot of discussion about some defining and naming conventions in graph theory, and I'd like to get some more opinions.

[Aaron Anderson]

• For relations such as the edge relation or the incidence of vertices on edges, I prefer a Prop-valued definition (V → V → Prop), and he prefered a set-valued definition (V → set V). These are definitionally equal, but does it matter which we use?
• It is also useful to have finset-valued versions, given some fintype instances. At that point, there are several versions of the same thing floating around, and they all have to have distinct names.

[Aaron Anderson]

As building out more combinatorics will have a lot of variations on these themes, I'd like to have a consistent guideline. Also, probably there are actually analogies in mathlib already, but I haven't identified them yet. I think my preference is the following, but this just lines up with what I've found convenient this summer:

[Aaron Anderson]

• The original definition is Prop-valued, and is given as simple a name as possible, like G.adj v w or v ~[G] w
• To get the corresponding set, we use {w | G.adj v w} or similar, and it doesn't get a separate name
• To get the finset, which may require some bundled proofs and instances, we use the full name, like G.neighbors v

[Aaron Anderson]

Tagging @Scott Morrison just because you had useful reviews asking for consistency

[Scott Morrison]

As I started saying in my review, while V → V → Prop and V → set V are definitionally equal, it's best not to take constant advantage of that, as it ends up being hard to use: the set API expects you to "stay in the world of set" most of the time.

[Scott Morrison]

To me V → V → Prop feels like the safer choice because it makes the connections with other types of graphs (and categories) more transparent.