OAI/Geometry/EinsteinFour/OrientationCoverClosed.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Separation and countability of the compact smooth orientation cover.

  1. instance OAI.PositiveEinsteinFour.Geometry.orientationCover_t3Space line 18
  2. instance OAI.PositiveEinsteinFour.Geometry.orientationCover_secondCountable line 20
  3. instance OAI.PositiveEinsteinFour.Geometry.orientationCover_nonempty line 23