Darts with a fixed tail

The darts of a simple graph with tail u correspond to the neighbours of u: a dart is sent to its head, and a neighbour w to the dart u → w (SimpleGraph.dartOfNeighborSet).

Main definitions

• SimpleGraph.dartFstEquivNeighborSet: the equivalence between the darts with tail u and the neighbour set of u.

def SimpleGraph.dartFstEquivNeighborSet {V : Type u_1} {G : SimpleGraph V} (u : V) : { d : G.Dart // d.toProd.1 = u } ≃ ↑(G.neighborSet u)

The darts with tail u are the neighbours of u: a dart is sent to its head.

@[simp]

theorem SimpleGraph.coe_dartFstEquivNeighborSet_apply {V : Type u_1} {G : SimpleGraph V} (u : V) (d : { d : G.Dart // d.toProd.1 = u }) : ↑((dartFstEquivNeighborSet u) d) = (↑d).toProd.2

The neighbour attached to a dart with tail u is its head.

@[simp]

theorem SimpleGraph.coe_dartFstEquivNeighborSet_symm_apply {V : Type u_1} {G : SimpleGraph V} (u : V) (w : ↑(G.neighborSet u)) : ↑((dartFstEquivNeighborSet u).symm w) = G.dartOfNeighborSet u w

The dart attached to a neighbour w of u is the dart u → w.