Theorems · Inductive type · combinatorics
SimpleGraph.Dart
{V : Type u_1} → SimpleGraph V → Type u_1A 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."
- Defined in
- Mathlib.Combinatorics.SimpleGraph.Dart
- Cited by
- 109 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement · cited by 3,072
Cited by125
Results whose statement or proof uses this declaration.
- SimpleGraph.Walk.dartsstatement · cited by 74
- SimpleGraph.Dart.toProdstatement and proof · cited by 48
- SimpleGraph.Dart.edgestatement and proof · cited by 32
- SimpleGraph.Walk.ext_supportproof · cited by 14
- SimpleGraph.Dart.symmstatement and proof · cited by 14
- SimpleGraph.Dart.adjstatement and proof · cited by 13
- SimpleGraph.Walk.fst_mem_support_of_mem_edgesproof · cited by 9
- SimpleGraph.Walk.length_dartsstatement · cited by 9
- SimpleGraph.Walk.firstDartstatement · cited by 8
- SimpleGraph.Walk.ofDartsstatement and proof · cited by 8
- SimpleGraph.Walk.lastDartstatement · cited by 7
- SimpleGraph.Dart.casesOnstatement and proof · cited by 7