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.1

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.

F1givenchoose

2.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.

F1F2F3step 1.1

3.1

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

step 2.1∎

Depends on

Used by

Dependency tree · two levels

28 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

Ioan Mărcuț, Manifolds (2017 lecture notes), §§14.5, 15.1 (standard reference, not scraped)