OAI/Geometry/HyperbolicGroups/ActualOccurrenceShape.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 15) line 15
  2. instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 16) line 16
  3. instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 17) line 17
  4. instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 18) line 18
  5. abbrev OAI.HyperbolicObstruction.ConeSkeleton.enumTop line 20
  6. abbrev OAI.HyperbolicObstruction.ConeSkeleton.enumFan line 21
  7. abbrev OAI.HyperbolicObstruction.ConeSkeleton.enumSquare line 22
  8. abbrev OAI.HyperbolicObstruction.ConeSkeleton.enumSix line 23
  9. def OAI.HyperbolicObstruction.ConeSkeleton.occurrenceShape line 27

    Source documentation

    One index for every actual included trial, with all seven fan slots and no duplication of a top by its boundary cycle or by decoration coordinates.

    def occurrenceShape : Occurrences.Shape (Fintype.card (Top n w))
    (Fintype.card (Fan n w)) (Fintype.card (Square n w)) :=
…

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.Fan, OAI.HyperbolicObstruction.ConeSkeleton.Square

  10. def OAI.HyperbolicObstruction.ConeSkeleton.occurrenceValues line 35

    Source documentation

    The literal signed values at original field positions.

    def occurrenceValues : (occurrenceShape n w).Pos (Fintype.card (Six n d)) → Alphabet n
  | .inl a => ((enumTop n w).symm a).val loose
  | .inr (.inl ⟨b,f⟩) => ((enumFan n w).symm b).val.2 f
  | .inr (.inr (.inl ⟨e,f⟩)) => ((enumSquare n w).symm e).2.val f
  | .inr (.inr (.inr (e,i))) => ((enumSix n d).symm e).val i

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.occurrenceShape, OAI.HyperbolicObstruction.ConeSkeleton.Six, OAI.HyperbolicObstruction.ConeSkeleton.enumTop, OAI.HyperbolicObstruction.ConeSkeleton.loose, OAI.HyperbolicObstruction.ConeSkeleton.enumFan, OAI.HyperbolicObstruction.ConeSkeleton.enumSquare, OAI.HyperbolicObstruction.ConeSkeleton.enumSix

  11. lemma OAI.HyperbolicObstruction.ConeSkeleton.loose_unique line 41
  12. lemma OAI.HyperbolicObstruction.ConeSkeleton.fan_value_congr line 44
  13. lemma OAI.HyperbolicObstruction.ConeSkeleton.occurrence_core_value line 51
  14. abbrev OAI.HyperbolicObstruction.ConeSkeleton.OccurrenceTrial line 62
  15. def OAI.HyperbolicObstruction.ConeSkeleton.occurrenceTrial line 65
  16. lemma OAI.HyperbolicObstruction.ConeSkeleton.occurrence_row line 71
  17. lemma OAI.HyperbolicObstruction.ConeSkeleton.occurrenceTrial_injective line 87
  18. lemma OAI.HyperbolicObstruction.ConeSkeleton.occurrence_row_injective line 129
  19. lemma OAI.HyperbolicObstruction.ConeSkeleton.occurrence_present line 134