Compact and closed manifold predicates

This file packages the dimension-independent topological hypotheses used by manifold constructions. The chart structure is supplied by a ChartedSpace instance over the Euclidean half-space (boundary allowed) or the Euclidean space (boundaryless) model. Every charted space is a topological manifold (Mathlib's instance IsManifold I 0 M). The predicates retain this condition to record the chosen model and atlas, while their iff lemmas characterize them by the remaining conditions: T2Space, SecondCountableTopology, CompactSpace, and ConnectedSpace. The file also provides the standard surface and three-manifold specializations used by geometric-topology APIs.

def TauCeti.IsCompactConnectedManifold (n : ℕ) [NeZero n] (X : Type u_3) [TopologicalSpace X] [ChartedSpace (EuclideanHalfSpace n) X] : Prop

A compact, connected n-manifold, allowing a nonempty boundary, in the standard Euclidean half-space model.

@[simp]

theorem TauCeti.isCompactConnectedManifold_iff (n : ℕ) [NeZero n] (X : Type u_3) [TopologicalSpace X] [ChartedSpace (EuclideanHalfSpace n) X] : IsCompactConnectedManifold n X ↔ T2Space X ∧ SecondCountableTopology X ∧ CompactSpace X ∧ ConnectedSpace X

The defining separation, countability, compactness, and connectedness conditions for IsCompactConnectedManifold.

theorem TauCeti.isCompactConnectedManifold (n : ℕ) [NeZero n] (X : Type u_3) [TopologicalSpace X] [ChartedSpace (EuclideanHalfSpace n) X] [T2Space X] [SecondCountableTopology X] [CompactSpace X] [ConnectedSpace X] : IsCompactConnectedManifold n X

The usual compactness, connectedness, separation, and countability typeclasses supply IsCompactConnectedManifold n X.

def TauCeti.IsClosedConnectedManifold (n : ℕ) (X : Type u_3) [TopologicalSpace X] [ChartedSpace (EuclideanSpace ℝ (Fin n)) X] : Prop

A compact, connected, Hausdorff, second-countable, boundaryless topological n-manifold.

@[simp]

theorem TauCeti.isClosedConnectedManifold_iff (n : ℕ) (X : Type u_3) [TopologicalSpace X] [ChartedSpace (EuclideanSpace ℝ (Fin n)) X] : IsClosedConnectedManifold n X ↔ T2Space X ∧ SecondCountableTopology X ∧ CompactSpace X ∧ ConnectedSpace X

The defining separation, countability, compactness, and connectedness conditions for IsClosedConnectedManifold.

theorem TauCeti.isClosedConnectedManifold (n : ℕ) (X : Type u_3) [TopologicalSpace X] [ChartedSpace (EuclideanSpace ℝ (Fin n)) X] [T2Space X] [SecondCountableTopology X] [CompactSpace X] [ConnectedSpace X] : IsClosedConnectedManifold n X

The usual compactness, connectedness, separation, and countability typeclasses supply IsClosedConnectedManifold n X.

def TauCeti.IsCompactConnectedSurface (S : Type u_3) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] : Prop

A compact connected surface, allowing a nonempty boundary, in the standard Euclidean half-space model.

def TauCeti.IsCompactConnectedThreeManifold (M : Type u_3) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace 3) M] : Prop

A compact connected 3-manifold, allowing a nonempty boundary, in the standard Euclidean half-space model.

@[simp]

theorem TauCeti.isCompactConnectedSurface_iff {S : Type u_1} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] : IsCompactConnectedSurface S ↔ T2Space S ∧ SecondCountableTopology S ∧ CompactSpace S ∧ ConnectedSpace S

The defining conditions for a compact connected surface.

@[simp]

theorem TauCeti.isCompactConnectedThreeManifold_iff {M : Type u_2} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace 3) M] : IsCompactConnectedThreeManifold M ↔ T2Space M ∧ SecondCountableTopology M ∧ CompactSpace M ∧ ConnectedSpace M

The defining conditions for a compact connected 3-manifold.

theorem TauCeti.isCompactConnectedSurface (S : Type u_3) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [T2Space S] [SecondCountableTopology S] [CompactSpace S] [ConnectedSpace S] : IsCompactConnectedSurface S

The usual compactness, connectedness, separation, and countability typeclasses supply the compact-connected-surface predicate.

theorem TauCeti.isCompactConnectedThreeManifold (M : Type u_3) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace 3) M] [T2Space M] [SecondCountableTopology M] [CompactSpace M] [ConnectedSpace M] : IsCompactConnectedThreeManifold M

The usual compactness, connectedness, separation, and countability typeclasses supply the compact-connected-3-manifold predicate.

def TauCeti.IsClosedConnectedSurface (S : Type u_3) [TopologicalSpace S] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) S] : Prop

A closed connected surface is a compact, connected, Hausdorff, second-countable, boundaryless topological 2-manifold. The dimension is pinned by the Euclidean 2-space model.

def TauCeti.IsClosedConnectedThreeManifold (M : Type u_3) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M] : Prop

A closed connected 3-manifold is a compact, connected, Hausdorff, second-countable, boundaryless topological 3-manifold.

@[simp]

theorem TauCeti.isClosedConnectedSurface_iff {S : Type u_1} [TopologicalSpace S] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) S] : IsClosedConnectedSurface S ↔ T2Space S ∧ SecondCountableTopology S ∧ CompactSpace S ∧ ConnectedSpace S

The defining separation, countability, compactness, and connectedness conditions for a closed connected surface.

@[simp]

theorem TauCeti.isClosedConnectedThreeManifold_iff {M : Type u_2} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M] : IsClosedConnectedThreeManifold M ↔ T2Space M ∧ SecondCountableTopology M ∧ CompactSpace M ∧ ConnectedSpace M

The defining separation, countability, compactness, and connectedness conditions for a closed connected 3-manifold.

theorem TauCeti.isClosedConnectedSurface (S : Type u_3) [TopologicalSpace S] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) S] [T2Space S] [SecondCountableTopology S] [CompactSpace S] [ConnectedSpace S] : IsClosedConnectedSurface S

The usual compactness, connectedness, separation, and countability typeclasses supply the closed-connected-surface predicate.

theorem TauCeti.isClosedConnectedThreeManifold (M : Type u_3) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M] [T2Space M] [SecondCountableTopology M] [CompactSpace M] [ConnectedSpace M] : IsClosedConnectedThreeManifold M

The usual compactness, connectedness, separation, and countability typeclasses supply the closed-connected-3-manifold predicate.