Nearest point of a convex subset of a Hilbert space

Let $𝑋$ be a Hilbert space and let $𝐴 \subseteq 𝑋$ be a inhabited, closed, convex subset. Then for any $𝑥 \in 𝑋$ there exists a unique $𝑎 \in 𝐴$ such that $‖ 𝑥 - 𝑎 ‖ = 𝑑 (𝑥, 𝐴)$ #m/thm/anal/fun where

𝑑 (𝑥, 𝐴) = i n f {‖ 𝑥 - 𝑎 ‖ : 𝑎 \in 𝐴}

Proof

#missing/proof

#state/develop | #lang/en | #SemBr