Nonzero element of minimal length in a lattice? Given two linearly independent vectors $a,b\in\mathbb{R}^2$ we form the lattice $L=\{ma+nb|m,n\in\mathbb{Z}\}$. Now, a proof starts with "choose a nonzero vector in $L$ of smallest length...". Why such a vector exists? In theory the lengths of vectors in $L$ can converge to 0.
Another formulation for the same question with different approach: I am trying to understand the crystallographic restriction theorem (given, e.g., in Armstrong, "Groups and Symmetry", chapter 25). The relevant definition of a crystallographic group is a group of plane isometries whose translation subgroup is generated by two vectors. Hence when this subgroup acts on the origin the resulting orbit is a lattice. Armstrong finds $a,b$ for this lattice by choosing $a$ to be the nonzero vector of smallest length; but again, why do such vector has to exist in the orbit?
 A: By turning the coordinate system, we can arrange things such that $a=(t,0)$ and $b=(p,q)$. Then, since $a$ and $b$ are linearly independent we must have $t\ne 0$ and $q\ne 0$ (but $p=0$ is possible).
It now ought to be clear that the $y$ coordinate of every lattice point must be a multiple of $q$, and that any lattice point with $y=0$ must be a multiple of $a$ alone.
Therefore, the lattice cannot contain any nonzero vector whose length is smaller than the minimum of $q$ and $t$. Such a vector would need to have $y=0$ (any nonzero multiple of $q$ would already make it too long), but then it is a multiple of $a$, and the shortest nonzero multiple of $a$ is $a$ itself, which is also too long.
Now let $\lambda$ be the infimum of all nonzero lengths of vectors in the lattice. There must be at least one vector whose lengths is $\lambda$, because otherwise the annulus between radii $\lambda$ and $\lambda+\epsilon$ around the origin would have to contain infinitely many lattice points, and there is not space for that many when any two points must be at least $\min(t,q)$ apart.
