OAI/Geometry/HyperbolicGroups/RelativeFanLink.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.SelectedTop line 25

    Source documentation

    ALL selected top polygons incident to this fan occurrence, not only those whose boundary actually visits it. This implements source03's nominal weight.

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

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top

  2. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.ApexInstance line 29

    Source documentation

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

    abbrev ApexInstance := {z : P.Vertex //
…
  3. instance OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.(instance at line 33) line 33
  4. instance OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.(instance at line 34) line 34
  5. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selectedOccurrence line 36
  6. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selectedOccurrence_kind line 39
  7. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.instance_start line 43
  8. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.instance_apex line 49
  9. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selectedTopAt line 53
  10. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.fragmentMark line 66
  11. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.mark_absent line 74
  12. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.mark_top_face line 79
  13. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.mark_top_index line 87
  14. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.mark_triangle_corner line 104
  15. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.fragment_represented line 114
  16. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.fragment_card line 119
  17. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.fragment_no_fixed line 124
  18. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.fragment_bipartite line 135
  19. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.fragment_no_backtrack line 143
  20. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.fragment_no_same_side line 153
  21. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.fragment_unique_turn line 165