OAI/Geometry/EinsteinFour/Classification.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PositiveEinsteinFour.classification line 13

   Source documentation

   Every closed connected Einstein four-manifold with strictly positive sectional curvature is isometric, after positive scaling, to the round sphere, complex projective plane, or real projective four-space.

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

   theorem classification (M : Type*) [TopologicalSpace M] [ChartedSpace FourSpace M]
       [IsManifold I4 ∞ M] [T2Space M] [SecondCountableTopology M]
       [CompactSpace M] [ConnectedSpace M] (g : SmoothMetric M)
       (hEinstein : IsEinstein g) (hpositive : HasPositiveSectionalCurvature g) :
       ∃ a : ℝ, 0 < a ∧
         (ScaledIsometricTo g a roundDistance ∨
           ScaledIsometricTo g a fubiniStudyDistance ∨
           ScaledIsometricTo g a realProjectiveDistance) :=
   …