Approximation property of an infimum (source code)

= Approximation property of an infimum
{title2=$\forall\varepsilon>0\;\exists a\in A:\ \ell\leq a<\ell+\varepsilon$}

Let $A\subseteq\mathbb R$ be nonempty and bounded below. A <lower bound> $\ell$ equals $\inf A$ exactly when every $\varepsilon>0$ admits $a\in A$ with $\ell\leq a<\ell+\varepsilon$. Otherwise $\ell+\varepsilon$ would be a larger <lower bound>. Taking tolerances $1/n$ gives a <sequence> of members converging to $\ell$. For a real-valued objective with finite <infimum>, this supplies a <minimizing sequence> without assuming that a <global minimizer> exists.