Darts in graphs

A Dart or half-edge or bond in a graph is an ordered pair of adjacent vertices, regarded as an oriented edge. This file defines darts and proves some of their basic properties.

structure SimpleGraph.Dart {V : Type u_1} (G : SimpleGraph V) extends V × V : Type u_1

A Dart is an oriented edge, implemented as an ordered pair of adjacent vertices. This terminology comes from combinatorial maps, and they are also known as "half-edges" or "bonds."

• fst : V
• snd : V
• adj : G.Adj self.toProd.1 self.toProd.2

instance SimpleGraph.instDecidableEqDart {V✝ : Type u_2} {G✝ : SimpleGraph V✝} [DecidableEq V✝] : DecidableEq G✝.Dart

def SimpleGraph.instDecidableEqDart.decEq {V✝ : Type u_2} {G✝ : SimpleGraph V✝} [DecidableEq V✝] (x✝ x✝¹ : G✝.Dart) : Decidable (x✝ = x✝¹)

theorem SimpleGraph.Dart.ext_iff {V : Type u_1} {G : SimpleGraph V} (d₁ d₂ : G.Dart) : d₁ = d₂ ↔ d₁.toProd = d₂.toProd

theorem SimpleGraph.Dart.ext {V : Type u_1} {G : SimpleGraph V} (d₁ d₂ : G.Dart) (h : d₁.toProd = d₂.toProd) : d₁ = d₂

@[simp]

theorem SimpleGraph.Dart.fst_ne_snd {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) : d.toProd.1 ≠ d.toProd.2

@[simp]

theorem SimpleGraph.Dart.snd_ne_fst {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) : d.toProd.2 ≠ d.toProd.1

theorem SimpleGraph.Dart.toProd_injective {V : Type u_1} {G : SimpleGraph V} : Function.Injective toProd

instance SimpleGraph.Dart.fintype {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] : Fintype G.Dart

def SimpleGraph.Dart.edge {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) : Sym2 V

The edge associated to the dart.

@[simp]

theorem SimpleGraph.Dart.edge_mk {V : Type u_1} {G : SimpleGraph V} {p : V × V} (h : G.Adj p.1 p.2) : { toProd := p, adj := h }.edge = s(p.1, p.2)

@[simp]

theorem SimpleGraph.Dart.edge_mem {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) : d.edge ∈ G.edgeSet

def SimpleGraph.Dart.symm {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) : G.Dart

The dart with reversed orientation from a given dart.

@[simp]

theorem SimpleGraph.Dart.symm_toProd {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) : d.symm.toProd = d.swap

@[simp]

theorem SimpleGraph.Dart.symm_mk {V : Type u_1} {G : SimpleGraph V} {p : V × V} (h : G.Adj p.1 p.2) : { toProd := p, adj := h }.symm = { toProd := p.swap, adj := ⋯ }

@[simp]

theorem SimpleGraph.Dart.edge_symm {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) : d.symm.edge = d.edge

@[simp]

theorem SimpleGraph.Dart.edge_comp_symm {V : Type u_1} {G : SimpleGraph V} : edge ∘ symm = edge

@[simp]

theorem SimpleGraph.Dart.symm_symm {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) : d.symm.symm = d

@[simp]

theorem SimpleGraph.Dart.symm_involutive {V : Type u_1} {G : SimpleGraph V} : Function.Involutive symm

theorem SimpleGraph.Dart.symm_ne {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) : d.symm ≠ d

theorem SimpleGraph.dart_edge_eq_iff {V : Type u_1} {G : SimpleGraph V} (d₁ d₂ : G.Dart) : d₁.edge = d₂.edge ↔ d₁ = d₂ ∨ d₁ = d₂.symm

theorem SimpleGraph.dart_edge_eq_mk'_iff {V : Type u_1} {G : SimpleGraph V} {d : G.Dart} {u v : V} : d.edge = s(u, v) ↔ d.toProd = (u, v) ∨ d.toProd = (v, u)

theorem SimpleGraph.dart_edge_eq_mk'_iff' {V : Type u_1} {G : SimpleGraph V} {d : G.Dart} {u v : V} : d.edge = s(u, v) ↔ d.toProd.1 = u ∧ d.toProd.2 = v ∨ d.toProd.1 = v ∧ d.toProd.2 = u

def SimpleGraph.DartAdj {V : Type u_1} (G : SimpleGraph V) (d d' : G.Dart) : Prop

Two darts are said to be adjacent if they could be consecutive darts in a walk -- that is, the first dart's second vertex is equal to the second dart's first vertex.

def SimpleGraph.dartOfNeighborSet {V : Type u_1} (G : SimpleGraph V) (v : V) (w : ↑(G.neighborSet v)) : G.Dart

For a given vertex v, this is the bijective map from the neighbor set at v to the darts d with d.fst = v.

@[simp]

theorem SimpleGraph.dartOfNeighborSet_toProd {V : Type u_1} (G : SimpleGraph V) (v : V) (w : ↑(G.neighborSet v)) : (G.dartOfNeighborSet v w).toProd = (v, ↑w)

theorem SimpleGraph.dartOfNeighborSet_injective {V : Type u_1} (G : SimpleGraph V) (v : V) : Function.Injective (G.dartOfNeighborSet v)

instance SimpleGraph.nonempty_dart_top {V : Type u_1} [Nontrivial V] : Nonempty ⊤.Dart