OAI/Geometry/HyperbolicGroups/RelativeRawPosition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.stepPosition line 21

   Source documentation

   The outside has no occurrence position. Its letters are genuine boundary penalties, and cannot be silently identified with a random row field.

   def stepPosition : WalkStep n w d ⊕ (walkTarget n w d c hc f).ExteriorSide ell hell
       (letterDart n w ∘ word) (letterWordClosed n w ell word) → Option (RawPosition n w d)
     | .inl s => some (rawPosition n w d s)
     | .inr _ => none
   
   variable (P : WalkPicture.{0} (target n w d ell hell word c hc f))

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.WalkStep, OAI.HyperbolicObstruction.ConeSkeleton.walkTarget, OAI.HyperbolicObstruction.ConeSkeleton.letterDart, OAI.HyperbolicObstruction.ConeSkeleton.letterWordClosed, OAI.HyperbolicObstruction.ConeSkeleton.RawPosition, OAI.HyperbolicObstruction.ConeSkeleton.rawPosition, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.target

2. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.stepPosition_some line 28
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.raw_position_once_per_face line 35
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.contact_position_different line 56