OAI/Geometry/Relativity/CKS/RoundReferenceJets.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSAngularGeometry.stereoFactor line 11
  2. def OAI.CKSAngularGeometry.stereoMetric line 13
  3. lemma OAI.CKSAngularGeometry.stereoFactor_positive line 15
  4. lemma OAI.CKSAngularGeometry.stereoFactor_smooth line 19
  5. lemma OAI.CKSAngularGeometry.stereoMetric_smooth line 25
  6. lemma OAI.CKSAngularGeometry.stereoMetric_det_positive line 27
  7. lemma OAI.CKSAngularGeometry.actualJet_continuous line 30
  8. def OAI.CKSAngularGeometry.roundReference line 57
  9. def OAI.CKSAngularGeometry.roundReferenceFamily line 59
  10. lemma OAI.CKSAngularGeometry.roundReference_continuous line 61
  11. lemma OAI.CKSAngularGeometry.roundReferenceFamily_compact line 65
  12. lemma OAI.CKSAngularGeometry.roundReferenceFamily_regular line 68
  13. theorem OAI.CKSAngularGeometry.round_uniform_operators line 72