Theorems · Definition · combinatorics
SimpleGraph.Walk.mapLe
{V : Type u} → {G G' : SimpleGraph V} → G ≤ G' → {u v : V} → G.Walk u v → G'.Walk u vThe specialization of SimpleGraph.Walk.map for mapping walks to supergraphs.
- Cited by
- 26 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.mapproof · cited by 66
- SimpleGraph.Hom.ofLEproof · cited by 27
Cited by26
Results whose statement or proof uses this declaration.
- SimpleGraph.Walk.isTrail_mapLestatement · cited by 3
- SimpleGraph.Walk.isCycle_mapLestatement · cited by 3
- SimpleGraph.Walk.isPath_mapLestatement · cited by 3
- SimpleGraph.Walk.isCircuit_mapLestatement · cited by 2
- SimpleGraph.egirth_antiproof · cited by 1
- SimpleGraph.Walk.IsPath.mapLestatement · cited by 1
- SimpleGraph.Walk.IsCycle.mapLestatement · cited by 1
- SimpleGraph.Walk.reverse_mapLestatement and proof · cited by 0
- SimpleGraph.Walk.mapLe_appendstatement and proof · cited by 0
- SimpleGraph.Walk.mapLe_isCyclestatement · cited by 0
- SimpleGraph.Walk.mapLe_isPathstatement · cited by 0
- SimpleGraph.Walk.mapLe.congr_simpstatement and proof · cited by 0