Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-13
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Closed embedded submanifolds of complete Riemannian manifolds are complete

Statement

Let (M,g) be a Riemannian manifold such that every connected component, with its Riemannian distance, is complete. Let S⊆M be a closed embedded submanifold and give S the induced Riemannian metric h=i∗g, where i:S↪M is the inclusion. Then every connected component of (S,h) is complete for its intrinsic Riemannian distance.

Thus closed embedded submanifolds of complete Riemannian manifolds are complete componentwise. In particular, if M and S are connected and (M,dg) is complete, then (S,dh) is a complete metric space.

Facts & Assumptions

Given: A Riemannian manifold (M,g) that is complete componentwise, a closed embedded submanifold S⊆M, its inclusion i, the induced metric h=i∗g, a connected component C of S, and a dh-Cauchy sequence (xn) in C.

[F1]

The inclusion of an embedded submanifold is a smooth embedding: The inclusion of an embedded submanifold is a smooth embedding. In particular, it is an immersion and identifies the submanifold topology with the ambient subspace topology.

[F2]

Pullback of a riemannian metric as a tensor: For a smooth map F and a Riemannian metric g, the pullback tensor satisfies (F∗g)p(v,w)=gF(p)(dFpv,dFpw).

[F3]

Pullback of a riemannian metric is riemannian exactly for immersions: The pullback of a Riemannian metric is Riemannian exactly when the map is an immersion.

[F4]

Riemannian distance on a connected manifold: On a connected Riemannian manifold, the distance between two points is the infimum of the lengths of piecewise-C1 curves joining them.

[F5]

The riemannian distance topology is the manifold topology: On every connected Riemannian manifold, convergence for the Riemannian distance is equivalent to convergence in the manifold topology, including at boundary points.

[F6]

Complete metric space: every Cauchy sequence converges in the space: A metric space is complete when every Cauchy sequence converges to a point of that space.

Proof

technique · direct
1.1F1F2F3F7given

By [F1], i is an immersion. Hence [F2] and [F3] show that h=i∗g is indeed a Riemannian metric on S. By [F7], the connected component C is open in S, so it is a connected submanifold and the restriction of h to C is again Riemannian.

2.1F2F4step 1.1

Let M0 be the connected component of M containing C. If γ is a piecewise-C1 curve in C, then [F2] gives pointwise equality of speeds and therefore Lh(γ)=Lg(i∘γ). Every such curve is also an ambient curve in M0. Taking the two infima in [F4] consequently gives dg(x,y)≤dh(x,y)(x,y∈C).

3.1F6step 2.1given

The inequality in step 2.1 makes (xn) a dg-Cauchy sequence in M0. By the assumed completeness of M0 and [F6], there is p∈M0 such that dg(xn,p)→0.

4.1F1F5step 3.1given

By [F5], xn→p in the manifold topology of M0. If p∉S, then M0∩(M∖S) would be an open neighbourhood of p in M0 containing none of the xn, contradicting this convergence. Thus p∈S. If O is any neighbourhood of p in S, [F1] gives an ambient-open V such that p∈S∩V⊆O. Since V∩M0 is a neighbourhood of p in M0, eventually xn∈V∩S⊆O. Hence xn→p in S.

5.1F7step 4.1

The component C is closed in S by [F7]. Since every xn lies in C and step 4.1 gives xn→p in S, closedness forces p∈C. Because C is also open in S, the same convergence is convergence in the manifold topology of C.

6.1F5F6step 1.1step 5.1∎

Apply [F5] to the connected Riemannian manifold C. Step 5.1 then gives dh(xn,p)→0. The arbitrary dh-Cauchy sequence (xn) therefore converges to a point of C, so [F6] proves that (C,dh) is complete. Since C was arbitrary, the componentwise statement and its connected special case follow.

Source locator

Datar, §19.1, printed pp. 139--141, supplies the Riemannian distance and local metric-topology comparison used through [F4] and [F5]. The closed-submanifold completion argument above is derived locally from the exact internal suppliers; it does not invoke Hopf--Rinow or any geodesic-completeness implication.

Boundary and choice audit

The empty submanifold has no nonempty component and the assertion is vacuous; the connected empty case has no sequences. In dimension zero, every connected component is a singleton. The same argument works unchanged in dimension one. Constant and eventually constant Cauchy sequences are included. Disconnected ambient manifolds and submanifolds are handled one component at a time. No endpoint assertion or equivalence is being made. No choice principle is used: the proof treats one arbitrary Cauchy sequence and invokes completeness once for that sequence.

Depends on

Used by

Dependency tree · two levels

34 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources