OAI/Geometry/EinsteinFour/RiemannianVolumePositive.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A nonempty smooth Riemannian four-manifold has positive Hausdorff volume. The proof compares a small neighborhood with its Euclidean chart using the actual Riemannian distance.

  1. theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_pos line 20
  2. theorem OAI.PositiveEinsteinFour.Geometry.actual_finitePositiveVolume line 55