OAI/Geometry/Relativity/CKS/CKSTensorFields.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CKSMixedGeometry.TensorFields line 13
  2. structure OAI.CKSMixedGeometry.TensorFields.RegularAt line 18
  3. def OAI.CKSMixedGeometry.tensorInputOf line 23
  4. def OAI.CKSMixedGeometry.tensorKField line 26
  5. def OAI.CKSMixedGeometry.tensorDenField line 29
  6. def OAI.CKSMixedGeometry.tensorLapseSqField line 32
  7. def OAI.CKSMixedGeometry.tensorLapseField line 35
  8. def OAI.CKSMixedGeometry.tensorCrossField line 38
  9. def OAI.CKSMixedGeometry.tensorQuadField line 41
  10. def OAI.CKSMixedGeometry.tensorLField line 44
  11. def OAI.CKSMixedGeometry.tensorEtaField line 48
  12. def OAI.CKSMixedGeometry.tensorTauField line 51
  13. lemma OAI.CKSMixedGeometry.tensorKField_diff line 55
  14. lemma OAI.CKSMixedGeometry.tensorDenField_diff line 62
  15. lemma OAI.CKSMixedGeometry.actual_tensorK line 69
  16. lemma OAI.CKSMixedGeometry.actual_tensorDen line 82
  17. lemma OAI.CKSMixedGeometry.actual_tensorLapseSq line 93
  18. lemma OAI.CKSMixedGeometry.actual_tensorLapse line 108