OAI/Geometry/Relativity/CKS/CollarRoundReferences.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSAngularGeometry.actualScalarJet_continuousAt line 13
  2. lemma OAI.CKSAngularGeometry.actualThreeJet_continuousAt line 27
  3. lemma OAI.CKSAngularGeometry.matrixThreeJets_continuous line 34
  4. def OAI.CKSAngularGeometry.roundShiftReference line 44
  5. def OAI.CKSAngularGeometry.roundShiftFamily line 45
  6. def OAI.CKSAngularGeometry.roundExpansionReference line 47
  7. def OAI.CKSAngularGeometry.roundExpansionFamily line 49
  8. lemma OAI.CKSAngularGeometry.roundShiftReference_continuous line 51
  9. lemma OAI.CKSAngularGeometry.roundShiftFamily_compact line 55
  10. lemma OAI.CKSAngularGeometry.roundShiftFamily_regular line 58
  11. lemma OAI.CKSAngularGeometry.roundExpansionReference_continuous line 62
  12. lemma OAI.CKSAngularGeometry.roundExpansionFamily_compact line 69
  13. lemma OAI.CKSAngularGeometry.roundExpansionFamily_regular line 72