TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-21

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.

Every open subset of $R^{n}$ admits a compact Jordan exhaustion

Statement

Every open subset of $R^{n}$ has a compact Jordan exhaustion.

Facts & Assumptions

Given: A natural $n \geq 1$ and an open set $D \subseteq R^{n}$ .

[L1]

If $C \subseteq U \subseteq R^{n}$ , where $C$ is compact and $U$ is open, then a compact Jordan set $K$ , which may be a finite union of closed grid rectangles, satisfies $C \subseteq int K \subseteq K \subseteq U$ (A compact subset of an open Euclidean set has a compact Jordan neighborhood inside that open set).

[L2]

For a nonempty set $A$ in a metric space, $∣ d (x, A) - d (y, A) ∣ \leq d (x, y)$ ( $∣ d (x, A) - d (y, A) ∣ \leq d (x, y)$ , so the distance to a fixed nonempty set is $1$ -Lipschitz).

[L3]

The rationals are countably infinite ( $Q$ is countably infinite).

[L4]

If $C$ is at most countable and $m \in N$ , then $C^{m}$ is at most countable (Every finite power of an at most countable set is at most countable).

[L5]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

[L6]

Recursion on $N$ produces a sequence from a seed and a specified successor function (The recursion theorem).

[L7]

A subset of $R^{n}$ is compact exactly when it is closed and bounded (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[L8]

The rationals are dense in $R$ (Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable).

[L9]

Jordan content is defined from finite rectangular inner families and outer covers, and the empty set has content zero (Jordan inner and outer content and Jordan measurable bounded sets in $R^{m}$ ).

[L10]

A closed box has volume equal to the product of its side lengths (Axis-parallel rectangles in $R^{m}$ and their volume).

[L11]

There is an explicit bijection $N \times N \to N$ ( $N \times N \approx N$ ).

Proof

technique · constructive

1.1

If $D = \emptyset$ , take $K_{j} = \emptyset$ for all $j$ ; [L9] verifies the Jordan clause. If $D = R^{n}$ , take $K_{j} = [- (j + 1), j + 1]^{n}$ ; [L7], [L9], and [L10] make these compact Jordan boxes. Both sequences are exhaustions, and the radii begin at $1$ .

L7L9L10construct

1.2

Suppose $D$ is proper and nonempty, put $F : = R^{n} ∖ D$ , and define $C_{j} : = {x \in R^{n} : ∣ x_{k} ∣ \leq j + 1 for every k < n, d (x, F) \geq 1 / (j + 1)}$ . By [L2], each $C_{j}$ is closed and bounded, hence compact by [L7], lies in $D$ , and satisfies $C_{j} \subseteq C_{j + 1}$ .

L2L7construct

1.3

Fix a bijection from $Q$ to $N$ using [L3]. Iterating the explicit pairing in [L11] codes every finite rational endpoint list by one natural, with its length included in the code; [L4] verifies each fixed-length stage. Thus all finite unions of closed rational grid rectangles admit one fixed enumeration by natural-number codes without Countable Choice.

L3L4L11

2.1

Apply [L1] to $C_{0} \subseteq D$ . Its finite grid union has a positive margin between the compact core and the complement of its interior and between the union and $R^{n} ∖ D$ . By [L8], move each of its finitely many grid endpoints by less than that margin to rational endpoints, preserving $C_{0} \subseteq int K_{0} \subseteq K_{0} \subseteq D$ . Thus the candidate codes of step 1.3 are nonempty, and [L5] selects their least member. The same argument applied to the compact set $C_{j + 1} \cup K$ defines a single-valued successor $K^{'}$ with $C_{j + 1} \cup K \subseteq int K^{'} \subseteq K^{'} \subseteq D$ .

step 1.2step 1.3L1L5L8construct

3.1

Apply [L6] to the seed $(0, K_{0})$ and the successor rule of step 2.1. The second coordinates form compact Jordan sets with $C_{j} \subseteq K_{j} \subseteq int K_{j + 1} \subseteq D$ .

step 1.3step 2.1L6construct

4.1

If $C \subseteq D$ is compact, [L7] bounds all of its coordinates. Also, open balls contained in $D$ cover $C$ ; a finite subcover and the minimum of their halved radii give a positive lower bound for $d (x, F)$ on $C$ . Hence $C \subseteq C_{j} \subseteq K_{j}$ for some $j$ ; in particular every point of $D$ is eventually included, and $(K_{j})$ is an exhaustion.

step 1.2step 3.1L7discharge-construct∎

Depends on

Used by

An integrable dominator gives uniform tail control on every compact parameter set Lemma

Dependency tree · two levels

101 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

V. Guillemin, MIT 18.101 Analysis II Lecture Notes, Theorem 3.20 (standard reference, not scraped)

Every open subset of RnRn admits a compact Jordan exhaustion