OAI/Geometry/RCD/Coordinates/NormalizedHausdorffImage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Image bounds for the exact normalized Hausdorff measure

The normalization factor is the same in source and target. This does not identify the Euclidean target measure with Lebesgue measure.

  1. theorem OAI.RegularPointCoordinates.normalized_hausdorff_image_le line 18
  2. theorem OAI.RegularPointCoordinates.normalized_hausdorff_real_image_le line 29