Multigraph notation - naming poll

Stream: mathlib4

[Peter Nelson]

#24122 defines (undirected) multigraphs, as discussed in this PR review thread .

A few notational discussions have come up, which it makes sense to put to a poll.

First : multigraphs have vertex and edge types α and β, and two useful objects are predicates currently called Graph.Inc : β → α → Prop and Graph.Inc₂ : β → α → α → Prop - G.Inc e u means that u is one of the ends of the edge e in G, and G.Inc₂ e x y means that x and y are the two ends of the edge e in G (with appropriate nuances for loop edges).

Those names are mine, and I like that the names indicate their relationship. but at @Kyle Miller pointed out, the subscript in Inc₂ is a little awkward. Some other options for Inc₂ are G.Links e x y, G.IsLink e x y, G.IsEdgeFrom e x y, and also versions more suggestive of the picture where the edge goes in the middle such as G.IsLink x e y.

This is perhaps a little open-ended for a poll, but I'll follow this post with one.

[Eric Wieser]

Another option might be to just pick a name that looks nice in lemma names, but come up with a unicode notation which gives the right picture.

[Peter Nelson]

/poll How should the condition that e is an edge of G from x to y be named?
G.Inc₂ e x y
G.Link e x y
G.IsLink e x y
Something of the form _ x e y
A unicode notation, with link or similar in lemma names
Something else

[Eric Wieser]

Making some arguments into a set is yet another option, such as e ∈ G.edgesFrom x yor (x, y) ∈ G.linksOf e

[Peter Nelson]

I think that losing the dot notation would be too much to give up there.

[Eric Wieser]

Dot notation on h : G.IsEdgeFrom e x y you mean? Can you give an example?

[Peter Nelson]

From the PR. also Inc₂.adj, Inc₂.connected, etc etc.

lemma Inc₂.edge_mem (h : G.Inc₂ e x y) : e ∈ G.E :=
  (edge_mem_iff_exists_inc₂ ..).2 ⟨x, y, h⟩

lemma Inc₂.symm (h : G.Inc₂ e x y) : G.Inc₂ e y x :=
  G.inc₂_symm h.edge_mem h

lemma Inc₂.vx_mem_left (h : G.Inc₂ e x y) : x ∈ G.V :=
  G.vx_mem_left_of_inc₂ h

lemma Inc₂.vx_mem_right (h : G.Inc₂ e x y) : y ∈ G.V :=
  h.symm.vx_mem_left

[Peter Nelson]

A pertinent question : if the answer is unicode notation, then what notation? It would need to include all of G e x y. I don't love x ~[G,e] y (to make a random suggestion), but I can't imagine anything much simpler.

[Bhavik Mehta]

I'd also like unicode notation here but I don't have good ideas for it: yours has the problem that it makes G and e feel similar