OAI/Geometry/EinsteinFour/CP2UnitGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The unit representatives needed for the projective fixed-point argument.

  1. theorem OAI.PositiveEinsteinFour.cp2Overlap_of_unit_representatives line 13
  2. theorem OAI.PositiveEinsteinFour.cp2Overlap_eq_one_iff line 20
  3. theorem OAI.PositiveEinsteinFour.cp2_unit_aligned line 35
  4. theorem OAI.PositiveEinsteinFour.cp2_aligned_center line 60