OAI/Geometry/Relativity/CKS/SurfaceVolume.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSSurfaceVolume.chartFrame_eq_symmL line 24
  2. lemma OAI.CKSSurfaceVolume.chartFrame_continuousOn line 33
  3. lemma OAI.CKSSurfaceVolume.chartMatrix_continuousOn line 50
  4. lemma OAI.CKSSurfaceVolume.chartDensity_continuousOn line 60
  5. abbrev OAI.CKSSurfaceVolume.stdBasis line 73
  6. lemma OAI.CKSSurfaceVolume.sqrt_gram_det_comp line 75
  7. def OAI.CKSSurfaceVolume.pullbackInner line 89
  8. lemma OAI.CKSSurfaceVolume.chartMatrix_eq_toMatrix line 93
  9. theorem OAI.CKSSurfaceVolume.real_id_compTriple line 107
  10. def OAI.CKSSurfaceVolume.chartTransition line 111
  11. def OAI.CKSSurfaceVolume.transitionDeriv line 113
  12. lemma OAI.CKSSurfaceVolume.hasFDerivWithinAt_chartTransition line 116
  13. lemma OAI.CKSSurfaceVolume.chartFrame_comp_transitionDeriv line 124
  14. lemma OAI.CKSSurfaceVolume.pullbackInner_transition line 136
  15. lemma OAI.CKSSurfaceVolume.chartDensity_transition line 155
  16. lemma OAI.CKSSurfaceVolume.chart_target_measurable line 173
  17. def OAI.CKSSurfaceVolume.chartPreimage line 181
  18. lemma OAI.CKSSurfaceVolume.chartPreimage_measurable line 184
  19. lemma OAI.CKSSurfaceVolume.localVolume_apply line 193
  20. lemma OAI.CKSSurfaceVolume.chartTransition_image line 216
  21. lemma OAI.CKSSurfaceVolume.chartTransition_injOn line 241
  22. lemma OAI.CKSSurfaceVolume.localVolume_compatible line 248
  23. lemma OAI.CKSSurfaceVolume.exists_measure_of_compatible line 279
  24. theorem OAI.CKSSurfaceVolume.exists_volume line 307
  25. lemma OAI.CKSSurfaceVolume.volume_on_subset line 322
  26. lemma OAI.CKSSurfaceVolume.volume_locallyFinite line 329
  27. theorem OAI.CKSSurfaceVolume.exists_volume_locallyFinite line 363
  28. lemma OAI.CKSSurfaceVolume.measure_eq_of_restrict_cover line 377
  29. lemma OAI.CKSSurfaceVolume.measure_eq_of_chart_restrict line 399
  30. lemma OAI.CKSSurfaceVolume.volume_unique line 415
  31. lemma OAI.CKSSurfaceVolume.riemannianVolume_isVolume line 419
  32. instance OAI.CKSSurfaceVolume.riemannianVolume_locallyFinite line 421