OAI/Geometry/Relativity/CKS/SphereConeChart.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSSchwarzschild.sphereParam line 13
2. def OAI.CKSSchwarzschild.sphereParamDeriv line 14
3. lemma OAI.CKSSchwarzschild.sphereParam_norm line 16
4. lemma OAI.CKSSchwarzschild.sphereParamDeriv_orthogonal line 18
5. lemma OAI.CKSSchwarzschild.sphereParam_hasFDerivAt line 28
6. lemma OAI.CKSSchwarzschild.sphereParamDeriv_density line 40
7. def OAI.CKSSchwarzschild.sphereCone line 49
8. def OAI.CKSSchwarzschild.sphereConeDeriv line 50
9. lemma OAI.CKSSchwarzschild.sphereCone_hasFDerivAt line 52
10. lemma OAI.CKSSchwarzschild.sphereCone_det line 70