Theorems · Inductive type · combinatorics
SimpleGraph.Walk.Nil
{V : Type u} → {G : SimpleGraph V} → {v w : V} → G.Walk v w → PropPredicate for the empty walk.
Solves the dependent type problem where p = G.Walk.nil typechecks
only if p has defeq endpoints.
- Cited by
- 102 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement · cited by 3,072
- SimpleGraph.Walkstatement · cited by 915
Cited by107
Results whose statement or proof uses this declaration.
- SimpleGraph.Walk.adj_sndstatement and proof · cited by 15
- SimpleGraph.Walk.IsCycle.not_nilstatement and proof · cited by 14
- SimpleGraph.Walk.support_tail_of_not_nilstatement and proof · cited by 11
- SimpleGraph.Walk.firstDartstatement and proof · cited by 8
- SimpleGraph.Walk.lastDartstatement and proof · cited by 7
- SimpleGraph.Walk.not_nil_of_nestatement · cited by 7
- SimpleGraph.Walk.darts_eq_nilstatement · cited by 7
- SimpleGraph.Walk.eq_nil_iff_nilstatement · cited by 6
- SimpleGraph.Walk.adj_penultimatestatement and proof · cited by 6
- SimpleGraph.Walk.notNilRecstatement and proof · cited by 5
- SimpleGraph.Walk.cons_tail_eqstatement and proof · cited by 5
- SimpleGraph.Walk.Nil.eqstatement and proof · cited by 5