Theorems · Definition · combinatorics
SimpleGraph.Walk.drop
{V : Type u} → {G : SimpleGraph V} → {u v : V} → (p : G.Walk u v) → (n : ℕ) → G.Walk (p.getVert n) vThe walk obtained by removing the first n darts of a walk.
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 10 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.Walk.getVertstatement · cited by 114
- SimpleGraph.Walk.brecOnproof · cited by 15
Cited by31
Results whose statement or proof uses this declaration.
- SimpleGraph.Walk.tailproof · cited by 34
- SimpleGraph.Walk.isSubwalk_iff_support_isInfixproof · cited by 7
- SimpleGraph.Walk.drop_support_eq_support_drop_minstatement and proof · cited by 5
- SimpleGraph.Walk.isSubwalk_takeproof · cited by 4
- SimpleGraph.Walk.darts_dropUntil_suffix_dartsproof · cited by 4
- SimpleGraph.Walk.drop_getVertstatement and proof · cited by 4
- SimpleGraph.Walk.dropUntil_eq_dropstatement and proof · cited by 3
- SimpleGraph.Walk.drop_lengthstatement and proof · cited by 3
- SimpleGraph.Walk.isSubwalk_dropstatement · cited by 3
- SimpleGraph.Walk.darts_dropstatement and proof · cited by 2
- SimpleGraph.Walk.support_dropUntil_suffix_supportproof · cited by 2
- SimpleGraph.Walk.append_take_drop_eqstatement and proof · cited by 2