ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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.

The distance from a point to a nonempty compact set is attained at a point of that set, and two disjoint compact sets are at positive distance

Example

Let $(X, d)$ be a metric space (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric), with $d (x, A)$ and $d (A, B)$ the distances from a point to a nonempty set and between two nonempty sets (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space). Then:

If $K \subseteq X$ is nonempty and compact (Open cover, subcover, compact metric space, and compact subset of a metric space) and $x \in X$ , there is $a \in K$ with $d (x, a) = d (x, K)$ : the infimum defining the distance is attained.
If $K, L \subseteq X$ are nonempty, compact and disjoint, then $d (K, L) > 0$ , and again the value is attained at a point of $K$ .

Neither statement holds for arbitrary closed sets, and neither uses a choice principle.

Facts & Assumptions

Given: A metric space $(X, d)$ , nonempty compact subsets $K$ and $L$ of $X$ , and a point $x \in X$ .

[L1]

For nonempty $A \subseteq X$ , $d (x, A) = \inf {d (x, y) : y \in A}$ and $d (A, B) = \inf {d (u, v) : u \in A, v \in B}$ ; an infimum is a lower bound of its set and is at least every lower bound (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Greatest lower bound (infimum), Epsilon characterisation of the infimum).

[L2]

For nonempty $A \subseteq X$ the map $u \mapsto d (u, A)$ satisfies $∣ d (u, A) - d (v, A) ∣ \leq d (u, v)$ , so it is Lipschitz with constant $1$ and therefore continuous ( $∣ d (x, A) - d (y, A) ∣ \leq d (x, y)$ , so the distance to a fixed nonempty set is $1$ -Lipschitz, Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction, Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent, Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).

[L3]

A continuous real-valued function on a nonempty compact metric space attains a least value (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value); a subset is compact exactly when the corresponding metric subspace is, and the restriction of a continuous map to a subspace is continuous (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, Isometry, isometric embedding, and the subspace metric on a subset).

[L4]

A compact subset of a metric space is closed, and $u$ lies in the closure of a nonempty $A$ exactly when $d (u, A) = 0$ (A compact subset of a metric space is closed and bounded, The closure of a nonempty $A$ is ${x : d (x, A) = 0}$ , equals $A$ together with its limit points, and is the smallest closed superset, Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

[L5]

A minimum of a set of reals is a member of it and bounds it below (Maximum and minimum of a set).

Verification

technique · direct

1.1

The map $f : K \to R$ , $f (u) : = d (x, {u}) = d (x, u)$ , is the restriction to $K$ of $u \mapsto d (u, {x})$ , which is Lipschitz with constant $1$ and hence continuous; $K$ with the restricted metric is a nonempty compact metric space.

L2L3

2.1

So $f$ attains a least value at some $a \in K$ : $d (x, a) \leq d (x, u)$ for every $u \in K$ .

L3L5step 1.1

3.1

Hence $d (x, a)$ is a lower bound of ${d (x, u) : u \in K}$ that belongs to the set, so it is the infimum: $d (x, a) = d (x, K)$ , which is claim 1.

L1L5step 2.1

4.1

For claim 2, the map $g : K \to R$ , $g (u) : = d (u, L)$ , is continuous by the same argument, so it attains a least value at some $b \in K$ .

L2L3step 3.1

5.1

$g (b) > 0$ : otherwise $d (b, L) = 0$ would put $b$ in the closure of $L$ , which equals $L$ because $L$ is compact and hence closed, contradicting $K \cap L = \emptyset$ .

L4step 4.1

6.1

$d (K, L) = g (b)$ : every $u \in K$ and $v \in L$ satisfy $d (u, v) \geq d (u, L) \geq g (b)$ , so $g (b)$ is a lower bound of ${d (u, v) : u \in K, v \in L}$ ; and $d (K, L) \leq d (b, v)$ for every $v \in L$ , so $d (K, L)$ is a lower bound of ${d (b, v) : v \in L}$ and therefore $d (K, L) \leq d (b, L) = g (b)$ .

L1L5step 4.1step 5.1

7.1

Combining, $d (K, L) = g (b) > 0$ and the value is attained at $b \in K$ : claim 2.

step 5.1step 6.1∎

Remarks

Compactness is what makes the infimum a minimum. For a merely closed set the infimum need not be attained and disjoint closed sets can be at distance zero; what claim 1 uses is the extreme value theorem, and claim 2 additionally uses that a compact set is closed (A compact subset of a metric space is closed and bounded).

Only one of the two sets has to be compact for the attainment in claim 1, the point $x$ playing the role of a one-point compact set. In claim 2 compactness of $K$ gives the attainment and closedness of $L$ gives the positivity, which is why the proof calls on the two properties in different places.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 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

Compact space (Wikipedia) (standard reference, not scraped)
Extreme value theorem (Wikipedia) (standard reference, not scraped)