Lean Eval target theorem

This file contains the public theorem matching the Lean Eval problem statement.

theorem LeanEval.Topology.ClassificationOfSurfaces.classification_of_surfaces (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : Nonempty (S ≃ₜ SphereRepresentative) ∨ ∃ (p : ℕ) (n : ℕ), (1 ≤ p ∨ 1 ≤ n) ∧ Nonempty (S ≃ₜ Quot (OrientableRel p n)) ∨ 1 ≤ p ∧ Nonempty (S ≃ₜ Quot (NonOrientableRel p n))

Every compact connected Hausdorff topological 2-manifold with boundary is homeomorphic to the sphere, an orientable normal-form quotient, or a non-orientable normal-form quotient.

theorem LeanEval.Topology.ClassificationOfSurfaces.topological_classification_of_surfaces (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : Nonempty (S ≃ₜ SphereRepresentative) ∨ ∃ (p : ℕ) (n : ℕ), (1 ≤ p ∨ 1 ≤ n) ∧ Nonempty (S ≃ₜ Quot (OrientableRel p n)) ∨ 1 ≤ p ∧ Nonempty (S ≃ₜ Quot (NonOrientableRel p n))

Blueprint-facing spelling of classification_of_surfaces.