Theorems · Definition · combinatorics
SimpleGraph.Walk.darts
{V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → List G.DartThe darts of a walk is the list of darts it visits in order.
- Cited by
- 74 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Walkstatement and proof · cited by 915
- SimpleGraph.Dartstatement · cited by 109
- SimpleGraph.Walk.brecOnproof · cited by 15
Cited by75
Results whose statement or proof uses this declaration.
- SimpleGraph.Walk.edgesproof · cited by 145
- SimpleGraph.Walk.ext_supportproof · cited by 14
- SimpleGraph.Walk.fst_mem_support_of_mem_edgesproof · cited by 9
- SimpleGraph.Walk.length_dartsstatement and proof · cited by 9
- SimpleGraph.Walk.darts_eq_nilstatement and proof · cited by 7
- SimpleGraph.Walk.edges_reverseproof · cited by 6
- SimpleGraph.Walk.darts_bypass_sublist_dartsstatement and proof · cited by 4
- SimpleGraph.Walk.darts_copystatement and proof · cited by 4
- SimpleGraph.Walk.darts_dropUntil_suffix_dartsstatement and proof · cited by 4
- SimpleGraph.Walk.exists_boundary_dartstatement and proof · cited by 3
- SimpleGraph.Walk.dart_fst_mem_support_of_mem_dartsstatement and proof · cited by 3
- SimpleGraph.Walk.darts_appendstatement and proof · cited by 3