OAI/Geometry/HyperbolicGroups/MacroGroup.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.MacroGraph.route_exists line 12
2. def OAI.HyperbolicObstruction.MacroGraph.route line 32
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.macro_darts line 40
4. def OAI.HyperbolicObstruction.ConeSkeleton.macroValue line 73
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.macroValue_symm line 75
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.macro_cycle line 80
7. def OAI.HyperbolicObstruction.ConeSkeleton.macroPotential line 91
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.macroPotential_edge line 95