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

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.

Every point has a unique nearest point in a nonempty closed Euclidean convex set

Statement

Let $n \geq 1$ , let $C \subseteq R^{n}$ be nonempty, closed, and convex, and let $x \in R^{n}$ . Then there is a unique $p \in C$ such that $∥ x - p ∥_{2} \leq ∥ x - z ∥_{2}$ for every $z \in C$ .

Facts & Assumptions

Given: The set and point in the Statement. Closedness and convexity have the meanings of Interior, closure, boundary, limit point, isolated point and dense subset of a metric space and A convex subset of $R^{m}$ contains every line segment between two of its points, and distances come from The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ .

[L1]

For $n \geq 1$ , a subset of $R^{n}$ is compact if and only if it is closed and bounded (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).

[L2]

A continuous real function on a nonempty compact metric space attains a maximum and a minimum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[L3]

The Euclidean norm satisfies the parallelogram law (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

Proof

technique · contradiction

1.1

Choose $c_{0} \in C$ and put $R = ∥ x - c_{0} ∥_{2}$ . The set $K = C \cap \overline{B} (x, R)$ is nonempty, closed, and bounded, hence compact by [L1]. The continuous distance $z \mapsto ∥ x - z ∥_{2}$ attains a minimum at some $p \in K$ by [L2]. Points of $C ∖ K$ have distance greater than $R$ , so $p$ minimizes distance over all of $C$ .

L1L2givenchoose

2.1

Suppose distinct $p, q \in C$ both minimize the squared distance at $d^{2}$ . Convexity puts $(p + q) / 2$ in $C$ , while [L3] gives ${∥ x - \frac{p + q}{2} ∥}_{2}^{2} = d^{2} - \frac{1}{4} ∥ p - q ∥_{2}^{2} < d^{2},$ contradicting minimality. Thus the nearest point is unique.

step 1.1L3givenassume-contraalgebradischarge-contradiction∎

Depends on

Used by

Dependency tree · two levels

53 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

S. Boyd and L. Vandenberghe, Convex Optimization, §2.5.1 (standard reference, not scraped)
D. Bertsekas, MIT 6.253 Convex Analysis and Optimization, Lecture 6 (standard reference, not scraped)