LemmaStatement: AI-adaptedProof: 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.

A countable boundary coordinate cover has a locally finite shrinking

Statement

Assume the Axiom of Countable Choice. Let $(U_{n})_{n \geq 1}$ be a countable cover of a smooth manifold with boundary $M$ by relatively compact coordinate balls or half-balls. Then there is an at-most-countable index set $I$ and families of open sets $(W_{k})_{k \in I}$ and relatively compact coordinate balls or half-balls $(V_{k})_{k \in I}$ such that $M = ⋃_{k \in I} W_{k}$ , each $\overline{W_{k}} \subseteq V_{k} \subseteq \overline{V_{k}} \subseteq U_{n (k)}$ for some $n (k)$ , and $(V_{k})_{k \in I}$ is locally finite. The index set may be finite or empty.

Facts & Assumptions

Given: Countable Choice and a countable relatively compact coordinate ball or half-ball cover $(U_{n})$ of $M$ .

[L1]

At every point of a boundary manifold, relatively compact coordinate balls or half-balls form a basis subordinate to any open neighbourhood (Relatively compact coordinate balls and half-balls form a boundary-manifold basis).

[L3]

Compact subsets of Hausdorff spaces are closed, and closed subspaces of compact spaces are compact (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).

[L4]

Subsets of $N^{2}$ are at most countable ( $N \times N \approx N$ ).

[A1]

Smooth manifolds with boundary are Hausdorff.

[A2]

Countable Choice selects one finite covering list for each compact annulus from the nonempty set of all eligible finite lists (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

1.1givenL3

Put $H_{r} = ⋃_{i = 1}^{r} \overline{U_{i}}$ for $r \geq 1$ . Every $H_{r}$ is compact: an open cover of this finite union restricts to an open cover of each compact $\overline{U_{i}}$ , and the union of finitely many finite subcovers is finite. Also $U_{r} \subseteq int H_{r}$ , so the interiors of the $H_{r}$ cover $M$ .

2.1step 1.1construct

Set $r_{1} = 1$ . Given $r_{m}$ , compactness of $H_{r_{m}}$ and the increasing open cover $(int H_{r})_{r \geq 1}$ give an integer $r_{m + 1} > r_{m}$ with $H_{r_{m}} \subseteq int H_{r_{m + 1}}$ ; take the least such integer, so this recursion uses no additional choice. Put $K_{m} = H_{r_{m}}$ and $K_{- 1} = K_{0} = \emptyset$ . Then $K_{m} \subseteq int K_{m + 1}$ and the interiors of the $K_{m}$ cover $M$ .

3.1L1L3step 2.1

Let $A_{1} = K_{1}$ and $A_{m} = K_{m} ∖ int K_{m - 1}$ for $m \geq 2$ . Each $A_{m}$ is compact by [L3]. For each $m$ , consider every tuple $(n, W, V)$ with $V$ a coordinate ball or half-ball, $W$ open, and $\overline{W} \subseteq V \subseteq \overline{V} \subseteq U_{n} \cap int K_{m + 1} ∖ K_{m - 2} .$ Their $W$ -sets cover $A_{m}$ : given $x \in A_{m}$ , the displayed open neighbourhood contains $x$ for some $n$ ; use [L1] to take a relatively compact coordinate ball or half-ball $V$ with compact closure inside it, then apply [L1] again inside $V$ to take a ball or half-ball $W$ with $x \in W \subseteq \overline{W} \subseteq V$ . This proves pointwise existence without selecting witnesses at every point. Compactness makes the set of finite ordered tuple lists whose $W$ -sets cover $A_{m}$ nonempty; for an empty annulus, the empty list is eligible.

4.1A2L4step 2.1step 3.1

By [A2], choose one eligible finite ordered list for each $m$ . If its length is $s_{m}$ , index its tuples by pairs $(m, j)$ with $1 \leq j \leq s_{m}$ ; thus $I = {(m, j) : m \geq 1, 1 \leq j \leq s_{m}} \subseteq N^{2}$ is at most countable by [L4], and is empty when all lists are empty. Write these tuples as $(n (k), W_{k}, V_{k})$ . Since the annuli cover $M$ , so do the $W_{k}$ . For $y \in M$ , choose $m$ with $y \in int K_{m}$ . Any $V_{k}$ from annulus $A_{j}$ with $j \geq m + 3$ misses this neighbourhood because it lies outside $K_{j - 2} \supseteq K_{m}$ . Only finitely many tuples come from the finitely many earlier lists. Thus $(V_{k})$ is locally finite.

5.1step 3.1step 4.1∎

The constructed $W_{k}, V_{k}$ have the required nesting and cover, and $V_{k}$ is subordinate to an original $U_{n (k)}$ by its defining tuple.

Depends on

Dependency tree · 2 levels

Sources

Ioan Mărcuț, Manifolds (2017 lecture notes), §§14.5, 15.1; background for boundary charts and paracompact refinements