OAI/Geometry/HyperbolicGroups/WalkFacePosition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.free_sameface_not_opposite line 20
2. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.frozen_sameface_not_opposite line 36
3. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.normalized_index_inj line 48
4. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.normalized_sameface_not_opposite line 60
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.raw_position_once_per_face line 82

   Source documentation

   Every individual source face uses each indexed letter position at most once. For a top this uses simplicity AND absence of two-step polygons.

   lemma raw_position_once_per_face (hs : P.Simple) (hb : P.NoBigon)
       (hm : P.FrozenMapped (walkFrozenTarget n w d c hc f))
       {x y : P.Dart} (hxy : P.pairing.face.SameCycle x y)
       (hx : isLetter n w (walkLabel n w d (P.index x)) = true)
       (hy : isLetter n w (walkLabel n w d (P.index y)) = true)
       (hp : rawPosition n w d (P.index x) = rawPosition n w d (P.index y)) : x = y := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.walkFrozenTarget, OAI.HyperbolicObstruction.ConeSkeleton.isLetter, OAI.HyperbolicObstruction.ConeSkeleton.walkLabel, OAI.HyperbolicObstruction.ConeSkeleton.rawPosition