OAI/GroupTheory/FiniteType/SphereQuotient.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphereQuotient.Disk line 16
  2. abbrev OAI.SphereQuotient.Boundary line 17
  3. def OAI.SphereQuotient.height line 19
  4. def OAI.SphereQuotient.scale line 20
  5. theorem OAI.SphereQuotient.height_low line 22
  6. theorem OAI.SphereQuotient.scale_low line 25
  7. theorem OAI.SphereQuotient.height_mid line 30
  8. theorem OAI.SphereQuotient.scale_mid line 33
  9. theorem OAI.SphereQuotient.height_high line 37
  10. theorem OAI.SphereQuotient.scale_high line 40
  11. theorem OAI.SphereQuotient.scale_nonneg line 44
  12. def OAI.SphereQuotient.point line 48
  13. theorem OAI.SphereQuotient.point_norm line 51
  14. def OAI.SphereQuotient.quotient line 71
  15. def OAI.SphereQuotient.pole line 91
  16. theorem OAI.SphereQuotient.quotient_boundary line 94
  17. theorem OAI.SphereQuotient.height_eq_low_iff line 100
  18. theorem OAI.SphereQuotient.height_eq_high_iff line 110
  19. theorem OAI.SphereQuotient.profile_injective line 120
  20. theorem OAI.SphereQuotient.quotient_eq line 137
  21. theorem OAI.SphereQuotient.quotient_eq_pole line 159
  22. theorem OAI.SphereQuotient.boundary_ext line 170
  23. theorem OAI.SphereQuotient.quotient_surjective_or_pole line 176
  24. def OAI.SphereQuotient.sphereQuot line 250
  25. theorem OAI.SphereQuotient.sphereQuot_surjective line 254
  26. theorem OAI.SphereQuotient.sphereQuot_isQuotientMap line 260