OAI/Geometry/HyperbolicGroups/TriangleSquare.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

A literal closed triangle is the compact quotient of a square collapsing only its upper edge. Continuous face homotopies therefore descend with their three prescribed edge tracks.

  1. abbrev OAI.HyperbolicObstruction.TriangleSquare.Triangle line 15
  2. lemma OAI.HyperbolicObstruction.TriangleSquare.sum_coords line 17
  3. lemma OAI.HyperbolicObstruction.TriangleSquare.coord_le_one line 19
  4. instance OAI.HyperbolicObstruction.TriangleSquare.(instance at line 26) line 26
  5. def OAI.HyperbolicObstruction.TriangleSquare.quotient line 39
  6. lemma OAI.HyperbolicObstruction.TriangleSquare.quotient_zero line 53
  7. lemma OAI.HyperbolicObstruction.TriangleSquare.quotient_left line 55
  8. lemma OAI.HyperbolicObstruction.TriangleSquare.quotient_right line 57
  9. lemma OAI.HyperbolicObstruction.TriangleSquare.quotient_one line 59
  10. lemma OAI.HyperbolicObstruction.TriangleSquare.quotient_surjective line 62
  11. lemma OAI.HyperbolicObstruction.TriangleSquare.quotient_fiber line 82
  12. lemma OAI.HyperbolicObstruction.TriangleSquare.quotient_isQuotientMap line 95
  13. def OAI.HyperbolicObstruction.TriangleSquare.paramQuotient line 99
  14. lemma OAI.HyperbolicObstruction.TriangleSquare.paramQuotient_surjective line 100
  15. lemma OAI.HyperbolicObstruction.TriangleSquare.paramQuotient_isQuotientMap line 104
  16. lemma OAI.HyperbolicObstruction.TriangleSquare.fiber_constant line 110
  17. def OAI.HyperbolicObstruction.TriangleSquare.descend line 121
  18. lemma OAI.HyperbolicObstruction.TriangleSquare.descend_quotient line 129