OAI/Geometry/EinsteinFour/FrameBundle.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Actual orthonormal frames with the topology inherited from tangent vectors. Using the tangent-bundle topology is essential: chart coordinates at varying base points do not give a global product trivialization.

  1. structure OAI.PositiveEinsteinFour.Geometry.FrameBundle line 19

    Also declared: ComparatorChallenges/EinsteinFour.lean:125 (same declaration text).

  2. def OAI.PositiveEinsteinFour.Geometry.frameRealization line 23

    Distinct definitions of this name: ComparatorChallenges/EinsteinFour.lean:129 (same statement text; different proof or body). Qualify references as OAI.PositiveEinsteinFour.Geometry.frameRealization@path.

  3. instance OAI.PositiveEinsteinFour.Geometry.(instance at line 27) line 27
  4. theorem OAI.PositiveEinsteinFour.Geometry.continuous_frameRealization line 30
  5. theorem OAI.PositiveEinsteinFour.Geometry.continuous_frameBase line 34
  6. theorem OAI.PositiveEinsteinFour.Geometry.frameRealization_injective line 38
  7. theorem OAI.PositiveEinsteinFour.Geometry.isEmbedding_frameRealization line 57
  8. theorem OAI.PositiveEinsteinFour.Geometry.tangentBundle_t2Space line 63
  9. instance OAI.PositiveEinsteinFour.Geometry.(instance at line 80) line 80
  10. instance OAI.PositiveEinsteinFour.Geometry.(instance at line 84) line 84
  11. instance OAI.PositiveEinsteinFour.Geometry.(instance at line 87) line 87
  12. def OAI.PositiveEinsteinFour.Geometry.frameAt line 89
  13. theorem OAI.PositiveEinsteinFour.Geometry.frameBase_surjective line 92