OAI/Geometry/HyperbolicGroups/ActualLabel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.squareSide_field line 14
2. lemma OAI.HyperbolicObstruction.ConeSkeleton.square_value_congr line 21
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.representative_value line 27
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.raw_label_value line 49

   Source documentation

   Contact labels are compared only after forgetting orientation. Equal unsigned labels are not used to identify distinct indexed positions.

   lemma raw_label_value (s : WalkStep n w d) (hr : isLetter n w (walkLabel n w d s) = true) :
       (walkLabel n w d s).1 =
         .inl ((occurrenceValues n w d (rawToPosition n w d (rawPosition n w d s))).1) := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.WalkStep, OAI.HyperbolicObstruction.ConeSkeleton.isLetter, OAI.HyperbolicObstruction.ConeSkeleton.walkLabel, OAI.HyperbolicObstruction.ConeSkeleton.occurrenceValues, OAI.HyperbolicObstruction.ConeSkeleton.rawToPosition, OAI.HyperbolicObstruction.ConeSkeleton.rawPosition