Topological 3-manifolds

ClassTopological 3-manifold#✓fully proved

Let \(M\) be a topological space equipped with an atlas of charts, each a homeomorphism from an open subset of \(M\) onto an open subset of \(\mathbb{R}^3\), whose domains cover \(M\). Then \(M\) is a topological 3-manifold if it is Hausdorff and second-countable.

class IsThreeManifold (M : Type*) [TopologicalSpace M]
    [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M] : Prop
    extends T2Space M, SecondCountableTopology M

Used by 2

Used byCharacterization of topological 3-manifolds · Topological 3-manifolds are locally compact

ClassTopological 3-manifold with boundary#✓fully proved

A topological 3-manifold with boundary: a Hausdorff, second-countable topological space locally homeomorphic to the Euclidean half-space EuclideanHalfSpace 2.

class IsThreeManifoldWithBoundary (M : Type*) [TopologicalSpace M]
    [ChartedSpace (EuclideanHalfSpace 2) M] : Prop
    extends T2Space M, SecondCountableTopology M

TheoremCharacterization of topological 3-manifolds#✓fully proved

Let \(M\) be a topological space equipped with an atlas of charts modelled on \(\mathbb{R}^3\), so that \(M\) is locally homeomorphic to \(\mathbb{R}^3\). Then \(M\) is a topological 3-manifold if and only if \(M\) is Hausdorff and second-countable.

theorem isThreeManifold_iff [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M] :
    IsThreeManifold M ↔ T2Space M ∧ SecondCountableTopology M

Uses 1

Statement usesTopological 3-manifold

TheoremTopological 3-manifolds are locally compact#✓fully proved

Every topological 3-manifold \(M\) is locally compact, since \(\mathbb{R}^3\) is.

theorem IsThreeManifold.locallyCompactSpace [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M]
    [IsThreeManifold M] : LocallyCompactSpace M

Uses 1

Statement usesTopological 3-manifold

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.