TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck pass

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 triangle inequality and 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.1L1L2L3givenchoosealgebra

Choose $c_{0} \in C$ and put $R = 1 + ∥ x - c_{0} ∥_{2} > 0$ . Then $c_{0} \in K : = C \cap \overline{B} (x, R)$ , so $K$ is nonempty and bounded. The triangle inequality gives $∣ ∥ x - z ∥_{2} - ∥ x - w ∥_{2} ∣ \leq ∥ z - w ∥_{2}$ , hence the distance function is continuous. To see that the ball is closed directly, if $∥ z - x ∥_{2} > R$ , set $δ = (∥ z - x ∥_{2} - R) / 2 > 0$ ; whenever $∥ w - z ∥_{2} < δ$ , the triangle inequality gives $∥ w - x ∥_{2} \geq ∥ z - x ∥_{2} - ∥ w - z ∥_{2} > R$ . Thus its complement is open. Since $C$ is closed, the complement of $K$ is the union of two open sets and is open: each point retains a contained open ball from one member. Therefore $K$ is closed, and [L1] makes it compact. By [L2], the continuous distance attains a minimum at some $p \in K$ . Points of $C ∖ K$ have distance greater than $R$ , while $∥ x - p ∥_{2} \leq ∥ x - c_{0} ∥_{2} < R$ , so $p$ minimizes distance over all of $C$ .

2.1step 1.1L3givenassume-contraalgebradischarge-contradiction∎

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.

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

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources