OAI/Geometry/EinsteinFour/OrientationCoverTopology.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual orientation cover has a continuous free deck involution and exactly two points over each base point.

  1. abbrev OAI.PositiveEinsteinFour.Geometry.orientationCoverProjection line 18
  2. def OAI.PositiveEinsteinFour.Geometry.orientationCoverDeck line 21
  3. theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverDeck_proj line 23
  4. theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverDeck_deck line 26
  5. theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverDeck_free line 31
  6. theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_fibers line 36
  7. theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverProjection_surjective line 50
  8. def OAI.PositiveEinsteinFour.Geometry.orientationCoverFiberEquiv line 53
  9. theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_fiber_card line 64
  10. theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverDeck_localTriv line 69
  11. theorem OAI.PositiveEinsteinFour.Geometry.continuous_orientationCoverDeck line 78
  12. def OAI.PositiveEinsteinFour.Geometry.orientationCoverDeckHomeomorph line 104
  13. instance OAI.PositiveEinsteinFour.Geometry.orientationCover_t2Space line 112