OAI/Geometry/HyperbolicGroups/VoltageTriangleHomotopy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Extend the SAME coherent lifted graph contraction over each actual closed triangle. Its terminal map is based along all three sides.

  1. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.triangle_voltage line 23
  2. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.triangleSides line 28
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.triangleSides_initial line 41
  4. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.triangleSides_top line 56
  5. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.triangleHomotopy line 59
  6. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.triangleHomotopy_initial line 63
  7. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.triangleHomotopy_bottom line 65
  8. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.triangleHomotopy_left line 69
  9. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.triangleHomotopy_right line 73
  10. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.basedTriangle line 78
  11. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.basedTriangle_bottom line 79
  12. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.basedTriangle_left line 82
  13. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.basedTriangle_right line 85