Mathlib Map

Theorems · Definition · combinatorics

SimpleGraph.Reachable

{V : Type u} → SimpleGraph V → V → V → Prop

Two vertices are reachable if there is a walk between them. This is equivalent to Relation.ReflTransGen of G.Adj. See SimpleGraph.reachable_iff_reflTransGen.

Defined in
Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Cited by
141 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 4 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SimpleGraph.ConnectedComponent · cited by 86SimpleGraph.ConnectedComp…SimpleGraph.Preconnected · cited by 49SimpleGraph.PreconnectedSimpleGraph.connectedComponentMk · cited by 40SimpleGraph.connectedComp…SimpleGraph.IsBridge · cited by 30SimpleGraph.IsBridgeSimpleGraph.IsEdgeReachable · cited by 24SimpleGraph.IsEdgeReachab…SimpleGraph.Adj.reachable · cited by 17Adj.reachableSimpleGraph.Reachable.symm · cited by 15Reachable.symmSimpleGraph.Reachable.map · cited by 14Reachable.mapSimpleGraph.Reachable.trans · cited by 11Reachable.transSimpleGraph.Reachable.mono · cited by 10Reachable.monoSimpleGraph.Reachable.refl · cited by 10Reachable.reflSimpleGraph.ConnectedComponent.sound · cited by 9ConnectedComponent.soundSimpleGraph.Reachable.elim · cited by 7Reachable.elimSimpleGraph.Walk.reachable · cited by 7Walk.reachableSimpleGraph.ConnectedComponent.connected_toSimpleGraph · cited by 6ConnectedComponent.connec…SimpleGraph · cited by 3072SimpleGraphSimpleGraph.Walk · cited by 915SimpleGraph.WalkSimpleGraph.ReachableCITED 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.