OAI/Analysis/SymmetricDomains/FiniteCoveringRamifiedSection.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.finite_covering_lift_period line 34
  2. def OAI.Release061.PuncturedUnitDisk line 76
  3. instance OAI.Release061.(instance at line 78) line 78
  4. def OAI.Release061.halfPlaneQ line 80
  5. theorem OAI.Release061.continuous_halfPlaneQ line 83
  6. def OAI.Release061.halfPlaneInvQ line 86
  7. theorem OAI.Release061.halfPlaneQ_right_inv line 91
  8. theorem OAI.Release061.isOpenMap_halfPlaneQ line 96
  9. theorem OAI.Release061.isOpenQuotientMap_halfPlaneQ line 110
  10. def OAI.Release061.halfPlaneShift line 115
  11. theorem OAI.Release061.halfPlaneQ_shift line 123
  12. theorem OAI.Release061.halfPlaneShift_iterate line 131
  13. theorem OAI.Release061.halfPlaneShift_add line 143
  14. theorem OAI.Release061.halfPlaneShift_zero line 150
  15. theorem OAI.Release061.halfPlane_period_descent line 155
  16. def OAI.Release061.puncturedPower line 184
  17. theorem OAI.Release061.halfPlaneQ_nat line 190
  18. theorem OAI.Release061.finite_covering_ramified_section line 200