\begin{definition}[Definition:Sequence/Minimizing/Functional]
Let $y$ be a real mapping defined on a space $\MM$.
{{Stub|what is $\MM$?}}
Let $J \sqbrk y$ be a functional such that:
:$\exists y \in \MM: J \sqbrk y < \infty$
:$\ds \exists \mu > -\infty: \inf_y J \sqbrk y = \mu$
Let $\sequence {y_n}$ be a sequence such that:
:$\ds \lim_{n \mathop \to \infty} J \sqbrk {y_n} = \mu$
Then the sequence $\sequence {y_n}$ is called a '''minimizing sequence (of the functional $J \sqbrk y$)'''.
\end{definition}