OAI/GroupTheory/FiniteType/PresentationGeometryCells.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PresentationGeometry.Cells.old_fundamentalGroupMap_surjective line 17
  2. def OAI.PresentationGeometry.Cells.collarRetraction line 65
  3. theorem OAI.PresentationGeometry.Cells.collarRetraction_old line 67
  4. def OAI.PresentationGeometry.Cells.interiorLift line 71
  5. theorem OAI.PresentationGeometry.Cells.interiorLift_disk line 76
  6. theorem OAI.PresentationGeometry.Cells.overlapLift_half line 83
  7. def OAI.PresentationGeometry.Cells.overlapShell line 89
  8. theorem OAI.PresentationGeometry.Cells.overlapShell_continuous line 94
  9. def OAI.PresentationGeometry.Cells.overlapBoundary line 98
  10. theorem OAI.PresentationGeometry.Cells.collarToShell_overlap line 102
  11. theorem OAI.PresentationGeometry.Cells.collarRetraction_overlap line 108
  12. def OAI.PresentationGeometry.CellCoverExtension.baseSet line 123
  13. theorem OAI.PresentationGeometry.CellCoverExtension.mem_baseSet_old line 128
  14. theorem OAI.PresentationGeometry.CellCoverExtension.baseSet_isOpen line 137
  15. theorem OAI.PresentationGeometry.CellCoverExtension.mem_baseSet line 145
  16. def OAI.PresentationGeometry.CellCoverExtension.retractAt line 153
  17. theorem OAI.PresentationGeometry.CellCoverExtension.retractAt_collar line 157
  18. theorem OAI.PresentationGeometry.CellCoverExtension.retractAt_old line 161
  19. def OAI.PresentationGeometry.CellCoverExtension.overlapSection line 169
  20. theorem OAI.PresentationGeometry.CellCoverExtension.overlapSection_proj line 174
  21. def OAI.PresentationGeometry.CellCoverExtension.potential line 180
  22. def OAI.PresentationGeometry.CellCoverExtension.transition line 188
  23. def OAI.PresentationGeometry.CellCoverExtension.mixedCoordinate line 191
  24. theorem OAI.PresentationGeometry.CellCoverExtension.mixedCoordinate_formula line 211
  25. theorem OAI.PresentationGeometry.CellCoverExtension.transition_old_new line 229
  26. theorem OAI.PresentationGeometry.CellCoverExtension.transition_new_old line 238
  27. theorem OAI.PresentationGeometry.CellCoverExtension.continuousOn_transition line 246
  28. def OAI.PresentationGeometry.CellCoverExtension.coveringCore line 303
  29. theorem OAI.PresentationGeometry.CellCoverExtension.coveringCore_isCoveringMap line 313
  30. theorem OAI.PresentationGeometry.CellCoverExtension.coveringCore_old_coordChange line 316
  31. theorem OAI.PresentationGeometry.CellCoverExtension.mem_coveringCore_old line 322