Distance from a point to a closed set (source code)

= Distance from a point to a closed set

For a point $x$ and a nonempty <closed set> $A$ in a <metric space>, the distance
$$
d(x,A)=\inf_{a\in A}d(x,a)
$$
is a continuous function of $x$. It vanishes exactly on $A$.