Endpoints of an actual multigraph edge

This file associates to every actual edge of a multigraph the unordered pair of its actual vertices. It provides an endpoint interface that retains edge identities for parallel edges.

Main definition

• Graph.edgeEnds: the unordered pair of actual vertices at the ends of an actual edge.

noncomputable def Graph.edgeEnds {V : Type u_1} {E : Type u_2} (G : Graph V E) (e : ↑G.edgeSet) : Sym2 ↑G.vertexSet

The unordered pair of actual vertices at the ends of an actual edge.

@[simp]

theorem Graph.edgeEnds_eq_iff_isLink {V : Type u_1} {E : Type u_2} (G : Graph V E) (e : ↑G.edgeSet) (x y : ↑G.vertexSet) : G.edgeEnds e = s(x, y) ↔ G.IsLink ↑e ↑x ↑y

edgeEnds records exactly the IsLink relation of an actual edge.

@[simp]

theorem Graph.mem_edgeEnds_iff {V : Type u_1} {E : Type u_2} (G : Graph V E) (e : ↑G.edgeSet) (x : ↑G.vertexSet) : x ∈ G.edgeEnds e ↔ G.Inc ↑e ↑x

The vertices in edgeEnds e are exactly the vertices incident to e.