OAI/Geometry/HyperbolicGroups/WalkCover.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HyperbolicObstruction.PictureSwitch.WalkCellCover line 24

   Source documentation

   Literal voltage data for a regular cover of the indexed cell target. offset is the position of a side's initial vertex relative to its cell lift. These are local edge equations, not a chain-vanishing assumption.

   structure WalkCellCover (T : WalkCellTarget S C W L V A) (G : Type q) [Group G] where
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget

2. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkCellCover.offset_opposite_opposite line 36
3. def OAI.HyperbolicObstruction.PictureSwitch.WalkCellCover.target line 39
4. def OAI.HyperbolicObstruction.PictureSwitch.WalkCellCover.frozenTarget line 76
5. def OAI.HyperbolicObstruction.PictureSwitch.WalkCellCover.forget line 101

   Source documentation

   Forget deck coordinates but not a single dart or face.

   def forget : WalkPicture.{u} T where
   …

6. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkCellCover.deck_face line 110
7. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkCellCover.forget_simple line 114
8. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkCellCover.forget_noBigon line 125
9. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkCellCover.forget_fullyReduced line 127
10. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkCellCover.forget_radialInjective line 139
11. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkCellCover.forget_frozenMapped line 151