OAI/Geometry/HyperbolicGroups/MacroExceptional.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.ConeSkeleton.exceptionalMacro line 15
2. lemma OAI.HyperbolicObstruction.ConeSkeleton.macro_exceptional_port line 18
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.exceptional_successor line 33
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.exceptional_predecessor line 47
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.exceptional_next line 61
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.exceptional_previous line 77