OAI/Geometry/EinsteinFour/OrientationCoverCompactness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compactness of the actual two-sheeted orientation cover.

  1. theorem OAI.PositiveEinsteinFour.Geometry.exists_compact_orientationCover_neighborhood line 18
  2. instance OAI.PositiveEinsteinFour.Geometry.orientationCover_compactSpace line 36