LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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 set and a disjoint closed set have a positive norm-distance gap

Statement

Let $X$ be a real or complex normed space. If $K \subseteq X$ is nonempty compact, $C \subseteq X$ is nonempty closed, and $K \cap C = \emptyset$ , then there is $δ > 0$ with $∥ k - c ∥ \geq δ (k \in K, c \in C) .$ No convexity, completeness, HB, or infinite choice principle is required.

Facts & Assumptions

[F1]

Closed means open complement; an open set contains a positive-radius ball about each of its points (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

[F2]

A compact subset is compact for its restricted metric, so every intrinsic open cover has a finite subcover (Open cover, subcover, compact metric space, and compact subset of a metric space).

[F3]

A natural-number-indexed finite family of nonempty sets has a choice function in ZF (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

[F4]

Every nonempty finite list of real numbers has a maximum and a minimum (Every nonempty finite set of reals has a maximum and a minimum).

[F5]

The induced metric is $d (x, y) = ∥ x - y ∥$ over either scalar field, with the norm triangle inequality, using A norm on a real vector space, the induced metric, and the dictionary with the metric axioms over $R$ and Complex norm and complex normed space together with Realification preserves a complex norm and its metric over $C$ .

Proof

Given: A normed $X$ , nonempty compact $K$ , nonempty closed $C$ , and $K \cap C = \emptyset$ .

1.1givenF1

Form the set of all admissible pairs $T = {(a, r) \in K \times (0, \infty) : B (a, 3 r) \cap C = \emptyset}$ and the family $U = {K \cap B (a, r) : (a, r) \in T}$ . For each fixed $k \in K$ , the open complement of $C$ contains $k$ , so some $s > 0$ has $B (k, s) \cap C = \emptyset$ . Then $(k, s / 3) \in T$ and $k \in K \cap B (k, s / 3)$ . Thus $U$ covers $K$ without selecting radii for all $k$ simultaneously.

2.1step 1.1F1F5algebra

Each $V = K \cap B (a, r)$ in this family is open for the restricted metric on $K$ . Indeed, if $k \in V$ , then $r - ∥ k - a ∥ > 0$ , and every $y \in K$ with $∥ y - k ∥ < r - ∥ k - a ∥$ satisfies $∥ y - a ∥ \leq ∥ y - k ∥ + ∥ k - a ∥ < r$ , so is in $V$ . Thus $U$ is an intrinsic open cover of $K$ .

3.1step 1.1step 2.1F2F3

Compactness gives a finite subcover $V_{0}, \dots, V_{n - 1}$ with $n \geq 1$ , since $K \neq \emptyset$ . For each index $j < n$ define $W_{j} = {(a, r) \in T : V_{j} = K \cap B (a, r)}$ . Each $W_{j}$ is nonempty by the definition of $U$ . Applying finite choice to the function $j \mapsto W_{j}$ supplies pairs $(a_{j}, r_{j}) \in W_{j}$ for these finitely many indices. Repeated $V_{j}$ or $W_{j}$ cause no problem: a choice function on the set of values can be evaluated at each $W_{j}$ .

4.1step 3.1F4

The finite list $r_{0}, \dots, r_{n - 1}$ consists of positive reals, so its minimum $δ$ exists and is positive, since it equals one of those reals.

5.1step 3.1step 4.1F5algebra∎

For any $k \in K$ choose an index $j < n$ with $k \in V_{j}$ , possible because the finite family covers $K$ . For every $c \in C$ , admissibility gives $∥ c - a_{j} ∥ \geq 3 r_{j}$ , whereas $∥ k - a_{j} ∥ < r_{j}$ . Hence $∥ c - k ∥ \geq ∥ c - a_{j} ∥ - ∥ k - a_{j} ∥ > 2 r_{j} \geq δ$ . This proves the uniform bound for all $k, c$ .

Source notes

Brezis Theorem 1.7 proof, p.7, closed-minus-compact step expanded; Teschl Corollary 5.4 proof, p.140, finite-cover step specialized to normed spaces.

A compact set and a disjoint closed set have a positive norm-distance gap

Statement

Facts & Assumptions

Proof

Source notes

Depends on

Dependency tree · 2 levels

Sources