OAI/Geometry/EinsteinFour/RiemannianVolumeFinite.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compactness and bounded inverse-chart differentials imply finiteness of the actual four-dimensional Riemannian Hausdorff measure.

  1. theorem OAI.PositiveEinsteinFour.Geometry.fourSpace_hausdorff_haar line 19
  2. theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_lt_top line 25