Alphabeta Math
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⊆X is nonempty compact, C⊆X is nonempty closed, and K∩C=∅, then there is δ>0 with ∥k−c∥≥δ(k∈K, c∈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∩C=∅.

1.1givenF1

Form the set of all admissible pairs T={(a,r)∈K×(0,∞):B(a,3r)∩C=∅} and the family U={K∩B(a,r):(a,r)∈T}. For each fixed k∈K, the open complement of C contains k, so some s>0 has B(k,s)∩C=∅. Then (k,s/3)∈T and k∈K∩B(k,s/3). Thus U covers K without selecting radii for all k simultaneously.

2.1step 1.1F1F5algebra

Each V=K∩B(a,r) in this family is open for the restricted metric on K. Indeed, if k∈V, then r−∥k−a∥>0, and every y∈K with ∥y−k∥<r−∥k−a∥ satisfies ∥y−a∥≤∥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 V0,…,Vn−1 with n≥1, since K≠∅. For each index j<n define Wj={(a,r)∈T:Vj=K∩B(a,r)}. Each Wj is nonempty by the definition of U. Applying finite choice to the function j↦Wj supplies pairs (aj,rj)∈Wj for these finitely many indices. Repeated Vj or Wj cause no problem: a choice function on the set of values can be evaluated at each Wj.

4.1step 3.1F4

The finite list r0,…,rn−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∈K choose an index j<n with k∈Vj, possible because the finite family covers K. For every c∈C, admissibility gives ∥c−aj∥≥3rj, whereas ∥k−aj∥<rj. Hence ∥c−k∥≥∥c−aj∥−∥k−aj∥>2rj≥δ. 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.

Depends on

Used by

Dependency tree · two levels

33 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