OAI/Geometry/Relativity/CKS/SchwarzschildCKS.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CKSSchwarzschild.four_atLeastTwo line 14
  2. lemma OAI.CKSSchwarzschild.tensorPatch_zero_smooth line 19
  3. lemma OAI.CKSSchwarzschild.tensorPatch_metric_CKS line 25
  4. lemma OAI.CKSSchwarzschild.tensorPatch_second_CKS line 40
  5. def OAI.CKSSchwarzschild.tensorPatch line 55
  6. lemma OAI.CKSSchwarzschild.tensorPatch_covers line 71
  7. lemma OAI.CKSSchwarzschild.tensorPatch_realizes line 78
  8. lemma OAI.CKSSchwarzschild.tensorPatch_aspect line 86
  9. lemma OAI.CKSSchwarzschild.cksData_metric_smooth line 97
  10. lemma OAI.CKSSchwarzschild.cksData_tensor_smooth line 102
  11. lemma OAI.CKSSchwarzschild.cksData_represents line 107
  12. lemma OAI.CKSSchwarzschild.cksData_aspect_smooth line 130
  13. def OAI.CKSSchwarzschild.cksData line 133