OAI/Geometry/EinsteinFour/Statement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The classification target

The classification identifies a positively curved Einstein metric, after positive rescaling, with one of the three standard model distances.

  1. def OAI.PositiveEinsteinFour.Classified line 22

    Source documentation

    The three metric models in the manuscript's unoriented classification. a is the positive factor multiplying the original Riemannian metric.

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

    def Classified (g : SmoothMetric M) : Prop :=
…
  2. def OAI.PositiveEinsteinFour.ClassificationOn line 30

    Source documentation

    The family of main claims for a fixed smooth four-manifold. Compactness encodes "closed" since the model has no boundary.

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

    def ClassificationOn (M : Type*) [TopologicalSpace M] [ChartedSpace FourSpace M]
    [IsManifold I4 ∞ M] [T2Space M] [SecondCountableTopology M]
    [CompactSpace M] [ConnectedSpace M] : Prop :=
…