LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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 \geq 1$ . If $C \subseteq U \subseteq R^{n}$ , where $C$ is compact and $U$ is open, then there is a compact Jordan set $K$ such that $C \subseteq 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 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 $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).

[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 $R^{m}$ has content zero in $R^{m + 1}$ , A bounded set in $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 int R_{x}$ . The interiors cover $C$ , so [L1] selects $R_{1}, \dots, R_{N}$ . Put $K = ⋃_{i} R_{i}$ . Then $C \subseteq 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 · two levels

52 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

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