OAI/Geometry/RCD/Metric/InverseMeasureUnique.lean
1 declarations, 0 contain sorry, 0 declared as axioms
A common almost-everywhere inverse determines submeasures by their image
- theorem
OAI.RegularPointCoordinates.measure_eq_of_common_ae_inverseline 12