OAI/Geometry/HyperbolicGroups/PictureCotreeTree.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.complement_boundary_eq line 22
2. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.cotree_isTree line 37

   Source documentation

   The complement of ANY literal spanning-tree subpairing is a dual tree, not just the particular Kruskal forest supplied by tree_cotree. This is needed when the primal tree is chosen for a radius bound.

   theorem cotree_isTree (hG : M.GenusZero)
       (hspan : SameCycle.setoid M.vertex ⊔ SameCycle.setoid q = ⊤)
       (hboundary : cycles (M.vertex*q) = 1) : (M.cotreeGraph q hq).IsTree := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles