OAI/Geometry/Relativity/CKS/MeasureGlue.lean
1 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CKSIntrinsicVolume.exists_measure_of_compatibleline 9
OAI/Geometry/Relativity/CKS/MeasureGlue.lean1 declarations, 0 contain sorry, 0 declared as axioms
OAI.CKSIntrinsicVolume.exists_measure_of_compatible line 9