OAI/GroupTheory/FiniteType/SphereCover.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphereCover.Sphere line 16
  2. abbrev OAI.SphereCover.Cap line 17
  3. abbrev OAI.SphereCover.Orth line 18
  4. def OAI.SphereCover.capEquiv line 20
  5. lemma OAI.SphereCover.cap_contractible line 23
  6. lemma OAI.SphereCover.ne_neg line 25
  7. lemma OAI.SphereCover.cap_cover line 36
  8. abbrev OAI.SphereCover.Overlap line 45
  9. def OAI.SphereCover.antipode line 47
  10. lemma OAI.SphereCover.capEquiv_antipode line 49
  11. def OAI.SphereCover.overlapEquiv line 52
  12. def OAI.SphereCover.puncturedEquiv line 58
  13. def OAI.SphereCover.overlapHomotopyEquiv line 66
  14. def OAI.SphereCover.overlapInterEquiv line 70
  15. lemma OAI.SphereCover.overlap_pathConnected line 79
  16. theorem OAI.SphereCover.simplyConnected line 99
  17. def OAI.SphereCover.puncturedHomeomorph line 128
  18. def OAI.SphereCover.sphereHomotopyEquiv line 133
  19. lemma OAI.SphereCover.normed_simplyConnected line 137
  20. lemma OAI.SphereCover.normed_locallyPathConnected line 146
  21. def OAI.PresentationGeometry.Cells.boundaryProductEquiv line 155
  22. theorem OAI.PresentationGeometry.Cells.boundary_lift line 171
  23. def OAI.DiscreteCoverCharts.point line 205
  24. theorem OAI.DiscreteCoverCharts.point_proj line 208
  25. theorem OAI.DiscreteCoverCharts.point_val line 210
  26. theorem OAI.DiscreteCoverCharts.point_change line 213
  27. def OAI.DiscreteCoverCharts.chartPath line 219
  28. theorem OAI.DiscreteCoverCharts.chartPath_map line 227
  29. def OAI.DiscreteCoverCharts.fiberEquiv line 231
  30. theorem OAI.DiscreteCoverCharts.covering line 251
  31. theorem OAI.DiscreteCoverCharts.monodromy_chartPath line 253