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

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 compact subset of an open Euclidean set has a compact Jordan neighborhood inside that open set

Statement

Let $n\ge1$ . If $C\subseteq U\subseteq\mathbb R^n$ , where $C$ is compact and $U$ is open, then there is a compact Jordan set $K$ such that $C\subseteq\operatorname{int}K\subseteq K\subseteq U.$ The set $K$ can be chosen as a finite union of closed grid rectangles.

Facts & Assumptions

Given: Compact $C$ contained in open $U\subseteq\mathbb R^n$ .

[L1]

Compactness is intrinsic and supplies a finite subcover from every relative open cover (Open cover, subcover, compact metric space, and compact subset of a metric space, A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it).

[L2]

Closed bounded subsets of Euclidean space are compact (Heine-Borel in $\mathbb{R}^n$ : with the Euclidean metric a subset of $\mathbb{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).

[L3]

Continuous coordinate graphs have content zero, and a bounded set is Jordan measurable exactly when its boundary is null (The graph of a continuous function on a closed nondegenerate rectangle in $\mathbb{R}^m$ has content zero in $\mathbb{R}^{m+1}$ , A bounded set in $\mathbb{R}^m$ is Jordan measurable iff its boundary is null, equivalently of content zero).

Proof

technique · finite-cover

1.1

For each $x\in C$ , openness gives a closed grid rectangle $R_x\subseteq U$ with $x\in\operatorname{int}R_x$ . The interiors cover $C$ , so [L1] selects $R_1,\ldots,R_N$ . Put $K=\bigcup_iR_i$ . Then $C\subseteq\operatorname{int}K\subseteq K\subseteq U$ .

L1given

2.1

The finite union $K$ is closed and bounded, hence compact by [L2]. Its boundary is contained in the union of the boundaries of the $R_i$ . Each rectangular face is a continuous coordinate graph over a bounded rectangle and is null by [L3]; a finite union remains null.

L2L3step 1.1

3.1

The boundary criterion in [L3] now makes $K$ Jordan measurable. Subdividing the finitely many rectangles by their common coordinate endpoints expresses the same set as a finite union of closed cells from one grid.

L3step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 146 results over 28 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

A. Leibman, Multidimensional Real Analysis, §5.5 (standard reference, not scraped)