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.
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
instance
SimpleGraph.instDecidableEqDart
{V✝ : Type u_2}
{G✝ : SimpleGraph V✝}
[DecidableEq V✝]
:
DecidableEq G✝.Dart
Equations
- SimpleGraph.instDecidableEqDart = SimpleGraph.decEqDart✝
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 SimpleGraph.Dart.toProd
instance
SimpleGraph.Dart.fintype
{V : Type u_1}
{G : SimpleGraph V}
[Fintype V]
[DecidableRel G.Adj]
:
Fintype G.Dart
Equations
- One or more equations did not get rendered due to their size.
The edge associated to the dart.
Instances For
@[simp]
theorem
SimpleGraph.Dart.edge_mk
{V : Type u_1}
{G : SimpleGraph V}
{p : V × V}
(h : G.Adj p.1 p.2)
:
@[simp]
theorem
SimpleGraph.Dart.edge_mem
{V : Type u_1}
{G : SimpleGraph V}
(d : G.Dart)
:
d.edge ∈ G.edgeSet
The dart with reversed orientation from a given dart.
Equations
- d.symm = { toProd := d.swap, adj := ⋯ }
Instances For
@[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]
@[simp]
@[simp]
theorem
SimpleGraph.Dart.symm_involutive
{V : Type u_1}
{G : SimpleGraph V}
:
Function.Involutive SimpleGraph.Dart.symm
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.
Instances For
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
.
Equations
- G.dartOfNeighborSet v w = { toProd := (v, ↑w), adj := ⋯ }
Instances For
@[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)
Equations
- ⋯ = ⋯