OAI/Geometry/HyperbolicGroups/SubpairingGraph.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.swaps_fix_of_outside line 19
2. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.subpairingGraph line 32
3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.subpairing_reachable line 42
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.subpairing_connected line 60
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.subpairing_edge_card_le line 71