OAI/Geometry/Relativity/CKS/SphericalCharts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSSphericalChart.sphereParam line 12
  2. def OAI.CKSSphericalChart.thetaFrame line 14
  3. def OAI.CKSSphericalChart.phiUnit line 16
  4. def OAI.CKSSphericalChart.phiFrame line 17
  5. def OAI.CKSSphericalChart.chartVector line 19
  6. lemma OAI.CKSSphericalChart.sphereParam_smooth line 21
  7. lemma OAI.CKSSphericalChart.thetaFrame_smooth line 25
  8. lemma OAI.CKSSphericalChart.phiUnit_smooth line 29
  9. lemma OAI.CKSSphericalChart.phiFrame_smooth line 33
  10. lemma OAI.CKSSphericalChart.chartVector_smooth line 36
  11. lemma OAI.CKSSphericalChart.sphereParam_norm line 42
  12. lemma OAI.CKSSphericalChart.component_fderiv line 51
  13. lemma OAI.CKSSphericalChart.fderiv_sphereParam line 57
  14. lemma OAI.CKSSphericalChart.angular_chain line 73