OAI/Geometry/EinsteinFour/ComplexProjectiveTriangle.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The triangle inequality for the actual Fubini--Study distance on CP2.

  1. theorem OAI.PositiveEinsteinFour.Geometry.complex_unit_angle line 11
  2. theorem OAI.PositiveEinsteinFour.Geometry.fubiniStudyDistance_triangle line 15