LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-09-23 (Codex)

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.

Relatively compact coordinate balls and half-balls form a boundary-manifold basis

Statement

Let $M$ be a smooth $n$ -manifold with boundary, $p \in M$ , and $O \subseteq M$ an open neighbourhood of $p$ . There is a boundary chart $φ : U \to V \subseteq H^{n}$ and an open coordinate ball $B = φ^{- 1} (B (c, r) \cap H^{n})$ such that $p \in B \subseteq \overline{B} \subseteq O,$ and $\overline{B}$ is compact. At an interior point one may take $B (c, r) \subseteq int H^{n}$ ; at a boundary point the relative ball is a half-ball centred at $c = φ (p)$ on the boundary. For $n = 0$ the corresponding coordinate ball is the singleton ${p}$ . These balls and half-balls form a basis of the topology of $M$ .

Facts & Assumptions

Given: $M, p, O$ as in the statement.

[F1]

Boundary charts map open subsets of $M$ homeomorphically onto relatively open subsets of $H^{n}$ ; $M$ is Hausdorff (Smooth charts, atlases, and structures with boundary, Topological manifolds with boundary).

[F2]

Euclidean closed balls are compact, as are their closed intersections with $H^{n}$ (For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact, Euclidean upper half-space and its boundary).

[F3]

Continuous images of compact spaces are compact; compact subsets of Hausdorff spaces are closed; and closed subsets of compact spaces are compact (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset, In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones, A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact).

Proof

technique · direct

1.1F1givenchoose

Choose a boundary chart $φ : U \to V$ at $p$ and put $c = φ (p)$ . The set $φ (U \cap O)$ is relatively open in $H^{n}$ . For $n > 0$ , choose $r > 0$ so small that the relative closed ball $\overline{B (c, r)} \cap H^{n}$ lies in $φ (U \cap O)$ . If $c$ is interior, shrink $r$ further so $\overline{B (c, r)} \subseteq int H^{n}$ . If $c$ lies on the boundary, $B (c, r) \cap H^{n}$ is a relative half-ball. For $n = 0$ , use the one-point chart image.

2.1F1F2F3step 1.1

Let $B$ be the inverse image of the relative open ball from step 1.1, and let $C$ be the inverse image of its relative closed ball. By [F2], the relative closed ball is compact; the inverse chart is continuous, so [F3] makes its image $C$ compact in $M$ . As $M$ is Hausdorff, [F3] also makes $C$ closed there. Thus $p \in B \subseteq \overline{B} \subseteq C \subseteq O$ , and $\overline{B}$ is a closed subset of compact $C$ , hence compact by [F3]. In dimension zero the singleton chart image gives the same conclusion.

3.1step 2.1∎

Step 2.1 works for every point and every open neighbourhood, so these relatively compact coordinate balls and half-balls form a basis.

Depends on

Dependency tree · 2 levels

Sources

Ioan Mărcuț, Manifolds (2017 lecture notes), §§14.5, 15.1