OAI/Geometry/Relativity/CKS/CKSFoliationLeadingFields.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSMixedGeometry.leadingDField line 13
  2. def OAI.CKSMixedGeometry.leadingTField line 15
  3. def OAI.CKSMixedGeometry.leadingLapseField line 17
  4. def OAI.CKSMixedGeometry.leadingUField line 18
  5. lemma OAI.CKSMixedGeometry.leadingDField_diff line 20
  6. lemma OAI.CKSMixedGeometry.leadingTField_diff line 25
  7. lemma OAI.CKSMixedGeometry.leadingLapseField_diff line 30
  8. lemma OAI.CKSMixedGeometry.leadingUField_diff line 32
  9. lemma OAI.CKSMixedGeometry.leadingDField_realized line 36
  10. lemma OAI.CKSMixedGeometry.leadingTField_realized line 46
  11. lemma OAI.CKSMixedGeometry.leadingLapseField_realized line 61
  12. lemma OAI.CKSMixedGeometry.leadingUField_realized line 64