OAI/Geometry/HyperbolicGroups/BFSTree.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PlanarRecursion.exists_distance_parent line 15
2. theorem OAI.HyperbolicObstruction.PlanarRecursion.exists_bfs_tree line 35

   Source documentation

   A literal shortest-path spanning tree of a finite connected graph. Root distances are preserved exactly, not merely bounded by the number of vertices. This is the radius-control input for the planar separator.

   theorem exists_bfs_tree (G : SimpleGraph V) (hG : G.Connected) (root : V) :
       ∃ T : SimpleGraph V, T ≤ G ∧ T.IsTree ∧ ∀ v, T.dist root v = G.dist root v := by
   …