Documentation

Mathlib.Combinatorics.SimpleGraph.Dart

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."

Instances For
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
Equations
  • One or more equations did not get rendered due to their size.
def SimpleGraph.Dart.edge {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) :

The edge associated to the dart.

Equations
@[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 = Sym2.mk p
@[simp]
theorem SimpleGraph.Dart.edge_mem {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) :
def SimpleGraph.Dart.symm {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) :

The dart with reversed orientation from a given dart.

Equations
@[simp]
theorem SimpleGraph.Dart.symm_toProd {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) :
@[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) :
@[simp]
theorem SimpleGraph.Dart.symm_symm {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) :
d.symm.symm = d
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} {p : V × V} :
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) :

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.

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

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

Equations
@[simp]
theorem SimpleGraph.dartOfNeighborSet_toProd {V : Type u_1} (G : SimpleGraph V) (v : V) (w : (G.neighborSet v)) :