OAI/Geometry/HyperbolicGroups/PolygonContraction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A global continuous contraction of the literal polygon voltage cover, constructed by cochain correction and locally finite closed-cell gluing.

  1. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedEdgePrisms line 22
  2. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedFacePrism line 33
  3. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.obstructionWeight line 54
  4. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.obstructionCochain line 59
  5. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.obstructionCochain_self line 62
  6. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.obstructionCochain_reverse line 65
  7. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.obstructionCochain_triangle line 76
  8. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.contractionFace line 100
  9. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.threeFacePrism line 109
  10. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.coverContraction line 117
  11. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.coverContraction_initial line 121
  12. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.coverContraction_final line 124
  13. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.coverContraction_fixed line 128