OAI/Geometry/EinsteinFour/CP2InvolutionFixed.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Every involution of CP2 preserving its Fubini--Study distance has a fixed point. The proof uses only the three coordinate lines and the unique central line of a nonorthogonal orbit.

  1. theorem OAI.PositiveEinsteinFour.cp2_not_everywhere_orthogonal line 16
  2. theorem OAI.PositiveEinsteinFour.cp2_involutive_overlap_fixed line 51
  3. theorem OAI.PositiveEinsteinFour.cp2_involutive_isometry_fixed line 62