OAI/GroupTheory/FiniteType/CubeDisk.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CubeDisk.Disk line 15
  2. def OAI.CubeDisk.toDisk line 17
  3. def OAI.CubeDisk.toCube line 25
  4. theorem OAI.CubeDisk.toCube_toDisk line 35
  5. theorem OAI.CubeDisk.toDisk_toCube line 41
  6. def OAI.CubeDisk.homeomorph line 47
  7. theorem OAI.CubeDisk.norm_eq_one_of_boundary line 55
  8. theorem OAI.CubeDisk.boundary_of_norm_eq_one line 67
  9. def OAI.WeakSphere.loop line 95
  10. theorem OAI.WeakSphere.exists_disk_path line 101
  11. def OAI.WeakSphere.pathData line 125
  12. theorem OAI.WeakSphere.pathData_factors line 128
  13. theorem OAI.WeakSphere.sphere_nullhomotopic line 145
  14. abbrev OAI.SphereExtension.Disk line 180
  15. abbrev OAI.SphereExtension.Boundary line 181
  16. def OAI.SphereExtension.radial line 183
  17. def OAI.SphereExtension.zeroDisk line 191
  18. abbrev OAI.SphereExtension.ConeData line 193
  19. def OAI.SphereExtension.coneQuot line 195
  20. theorem OAI.SphereExtension.norm_radial line 199
  21. theorem OAI.SphereExtension.coneQuot_surjective line 206
  22. theorem OAI.SphereExtension.coneQuot_isQuotientMap line 220
  23. def OAI.SphereExtension.coneMap line 223
  24. theorem OAI.SphereExtension.radial_eq line 229
  25. theorem OAI.SphereExtension.coneMap_factors line 242
  26. theorem OAI.SphereExtension.exists_extension line 273