Theorems · Definition · combinatorics
SimpleGraph.Walk.penultimate
{V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → VThe penultimate vertex of a walk, or the only vertex in a nil walk.
- Cited by
- 48 results in Mathlib
- Foundations
- Depth 9 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.lengthproof · cited by 212
- SimpleGraph.Walk.getVertproof · cited by 114
Cited by50
Results whose statement or proof uses this declaration.
- SimpleGraph.Walk.dropLaststatement · cited by 20
- SimpleGraph.Walk.lastDartproof · cited by 7
- SimpleGraph.Walk.adj_penultimatestatement · cited by 6
- SimpleGraph.Walk.snd_reversestatement · cited by 5
- SimpleGraph.Walk.support_dropLaststatement · cited by 4
- SimpleGraph.Walk.concat_dropLaststatement and proof · cited by 2
- SimpleGraph.Walk.penultimate_cons_of_not_nilstatement and proof · cited by 2
- SimpleGraph.Walk.IsCycle.neighborSet_toSubgraph_endpointstatement · cited by 2
- SimpleGraph.Walk.support_dropLast_concatstatement · cited by 2
- SimpleGraph.Walk.IsPath.eq_penultimate_of_mem_edgesstatement · cited by 2
- SimpleGraph.Walk.support_tail_perm_support_dropLaststatement · cited by 1
- SimpleGraph.Walk.lastDart_toProdstatement · cited by 1