OAI/Geometry/Relativity/CKS/VolumeMeasurable.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CKSIntrinsicVolume.chart_target_measurableline 12 - def
OAI.CKSIntrinsicVolume.chartPreimageline 20 - lemma
OAI.CKSIntrinsicVolume.chartPreimage_measurableline 23 - lemma
OAI.CKSIntrinsicVolume.localVolume_applyline 32