Mathlib Map

Theorems · Inductive type · combinatorics

Quiver.RootedConnected

{V : Type u} → [Quiver V] → V → Prop

RootedConnected r means that there is a path from r to any other vertex.

Defined in
Mathlib.Combinatorics.Quiver.Arborescence
Cited by
2 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
Quiver
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Quiver.shortestPath · cited by 2Quiver.shortestPathQuiver.RootedConnected.recOn · cited by 0RootedConnected.recOnQuiver.shortestPath.congr_simp · cited by 0shortestPath.congr_simpQuiver.geodesicSubtree · cited by 0Quiver.geodesicSubtreeQuiver.shortest_path_spec · cited by 0Quiver.shortest_path_specQuiver.RootedConnected.casesOn · cited by 0RootedConnected.casesOnQuiver · cited by 405QuiverQuiver.RootedConnectedCITED BYCITES

Cites1

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

  • Quiverstatement · cited by 405

Cited by6

Results whose statement or proof uses this declaration.