OAI/Analysis/StrictMeans/Rebasing.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.isOpen_halfPlane line 29
  2. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_hasDeriv line 32
  3. def OAI.StrictInverseFirstPower.rebaseDiskFunction line 37
  4. lemma OAI.StrictInverseFirstPower.rebase_den_ne_zero line 41
  5. lemma OAI.StrictInverseFirstPower.rebaseDiskFunction_differentiableOn line 46
  6. lemma OAI.StrictInverseFirstPower.rebaseDiskFunction_injOn line 53
  7. lemma OAI.StrictInverseFirstPower.rebaseDiskFunction_zero line 64
  8. lemma OAI.StrictInverseFirstPower.rebaseDiskFunction_hasDerivAt_zero line 68
  9. def OAI.StrictInverseFirstPower.rebaseDiskMap line 86
  10. lemma OAI.StrictInverseFirstPower.rebaseDiskMap_extension line 91
  11. lemma OAI.StrictInverseFirstPower.rebaseDiskMap_normalized line 96
  12. def OAI.StrictInverseFirstPower.rebase line 107
  13. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_rebase line 110
  14. def OAI.StrictInverseFirstPower.cayleyHalfPlaneMap line 130
  15. lemma OAI.StrictInverseFirstPower.continuous_affineProduct line 135
  16. lemma OAI.StrictInverseFirstPower.continuous_rebaseDiskFunction line 141
  17. lemma OAI.StrictInverseFirstPower.continuous_rebase line 161
  18. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_of_cayley line 167
  19. lemma OAI.StrictInverseFirstPower.diskFamily_ext line 171
  20. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_rebase_deriv line 183
  21. lemma OAI.StrictInverseFirstPower.rebase_one line 198
  22. lemma OAI.StrictInverseFirstPower.rebase_assoc line 204
  23. def OAI.StrictInverseFirstPower.halfPlaneQ line 219
  24. lemma OAI.StrictInverseFirstPower.halfPlaneQ_ne_zero line 222
  25. lemma OAI.StrictInverseFirstPower.halfPlaneQ_I line 225
  26. lemma OAI.StrictInverseFirstPower.halfPlaneQ_rebase line 228
  27. lemma OAI.StrictInverseFirstPower.continuous_halfPlaneQ line 233