OAI/Geometry/Relativity/CKS/VolumeUnique.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSIntrinsicVolume.measure_eq_of_restrict_cover line 11
2. lemma OAI.CKSIntrinsicVolume.measure_eq_of_chart_restrict line 34
3. lemma OAI.CKSIntrinsicVolume.volume_unique line 52
4. lemma OAI.CKSIntrinsicVolume.riemannianVolume_isVolume line 56
5. instance OAI.CKSIntrinsicVolume.riemannianVolume_locallyFinite line 58