OAI/Geometry/HyperbolicGroups/BoundaryList.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.bypass_formPerm_head line 17
2. lemma OAI.HyperbolicObstruction.PictureSwitch.bypassPair_formPerm_head line 25
3. lemma OAI.HyperbolicObstruction.PictureSwitch.bypassPair_formPerm line 29
4. structure OAI.HyperbolicObstruction.PictureSwitch.IsBoundary line 38

   Source documentation

   An enumerated literal face boundary; the empty outside is allowed.

   structure IsBoundary (f : Perm D) (xs : List D) : Prop where
   …

5. lemma OAI.HyperbolicObstruction.PictureSwitch.formPerm_map_apply line 42
6. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.invariant line 58
7. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.iterate line 62
8. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.sameCycle line 76
9. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.mem_of_sameCycle line 88
10. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.disjoint line 106
11. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.map line 112