Mathlib Map

Theorems · Inductive type · combinatorics

SimpleGraph.Walk.IsPath

{V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → Prop

A path is a walk with no repeating vertices. Use SimpleGraph.Walk.IsPath.mk' for a simpler constructor.

Defined in
Mathlib.Combinatorics.SimpleGraph.Paths
Cited by
140 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SimpleGraph.Path · cited by 22SimpleGraph.PathSimpleGraph.Walk.IsPath.isTrail · cited by 8IsPath.isTrailSimpleGraph.Walk.IsPath.support_nodup · cited by 8IsPath.support_nodupSimpleGraph.Walk.IsPath.getVert_injOn · cited by 7IsPath.getVert_injOnSimpleGraph.Walk.IsPath.mk' · cited by 7IsPath.mk'SimpleGraph.Walk.isPath_def · cited by 6Walk.isPath_defSimpleGraph.Walk.isPath_reverse_iff · cited by 6Walk.isPath_reverse_iffSimpleGraph.Walk.isPath_of_isSubwalk · cited by 5Walk.isPath_of_isSubwalkSimpleGraph.Walk.cons_isPath_iff · cited by 5Walk.cons_isPath_iffSimpleGraph.Reachable.exists_isPath · cited by 4Reachable.exists_isPathSimpleGraph.Walk.isPath_iff_injective_get_support · cited by 4Walk.isPath_iff_injective…SimpleGraph.Connected.exists_isPath · cited by 4Connected.exists_isPathSimpleGraph.Walk.IsCycle.isPath_tail · cited by 4IsCycle.isPath_tailSimpleGraph.Walk.IsPath.of_append_left · cited by 4IsPath.of_append_leftSimpleGraph.Walk.IsPath.reverse · cited by 4IsPath.reverseSimpleGraph · cited by 3072SimpleGraphSimpleGraph.Walk · cited by 915SimpleGraph.WalkWalk.IsPathCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by147

Results whose statement or proof uses this declaration.