OAI/Geometry/HyperbolicGroups/WalkFragment.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.ConeSkeleton.macroVertex_fan_slot line 27
  2. abbrev OAI.HyperbolicObstruction.ConeSkeleton.SelectedTop line 36

    Source documentation

    ALL selected top polygons incident to this fan occurrence, not only those whose boundary actually visits it.

    abbrev SelectedTop := {z : P.Face // select z = true ∧ ∃ a : Top n w,
…

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top

  3. abbrev OAI.HyperbolicObstruction.ConeSkeleton.ApexInstance line 40

    Source documentation

    Actual source vertices over this fan, represented in the chosen fragment.

    abbrev ApexInstance := {z : P.Vertex //
…
  4. instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 44) line 44
  5. instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 45) line 45
  6. def OAI.HyperbolicObstruction.ConeSkeleton.selectedOccurrence line 47
  7. lemma OAI.HyperbolicObstruction.ConeSkeleton.selectedOccurrence_kind line 50
  8. lemma OAI.HyperbolicObstruction.ConeSkeleton.instance_start line 54
  9. lemma OAI.HyperbolicObstruction.ConeSkeleton.instance_apex line 60
  10. def OAI.HyperbolicObstruction.ConeSkeleton.selectedTopAt line 64
  11. def OAI.HyperbolicObstruction.ConeSkeleton.fragmentMark line 77
  12. lemma OAI.HyperbolicObstruction.ConeSkeleton.mark_absent line 85
  13. lemma OAI.HyperbolicObstruction.ConeSkeleton.mark_top_face line 90
  14. lemma OAI.HyperbolicObstruction.ConeSkeleton.mark_top_index line 98
  15. lemma OAI.HyperbolicObstruction.ConeSkeleton.mark_triangle_corner line 112
  16. lemma OAI.HyperbolicObstruction.ConeSkeleton.fragment_represented line 122
  17. lemma OAI.HyperbolicObstruction.ConeSkeleton.fragment_card line 127
  18. lemma OAI.HyperbolicObstruction.ConeSkeleton.fragment_no_fixed line 132
  19. lemma OAI.HyperbolicObstruction.ConeSkeleton.fragment_bipartite line 143
  20. lemma OAI.HyperbolicObstruction.ConeSkeleton.fragment_no_backtrack line 151
  21. lemma OAI.HyperbolicObstruction.ConeSkeleton.fragment_no_same_side line 161
  22. lemma OAI.HyperbolicObstruction.ConeSkeleton.fragment_unique_turn line 173