OAI/Geometry/HyperbolicGroups/RelativeLayers.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_top_layer line 26
2. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_square_layer line 31
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_six_layer line 36
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_fan_layer line 42
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_layer_bounds line 72