In untyped lambda calculus, if we define (as is common) the set $\Lambda$ of all $\lambda$-terms with:
\begin{align} &(1) & \text{if } u \in V, \text{then } u \in \Lambda \\ &(2) & \text{if } M \text{ and } N \in V, \text{then } (MN) \in \Lambda \\ &(3) & \text{if } u \in V \text{ and } M \in \Lambda, \text{then } (\lambda.u M) \in \Lambda \\ \end{align}
or in short using a grammar $$ \Lambda = V | (V.\Lambda) | (\Lambda \Lambda),$$
can we then prove that all $\lambda$-terms are 'finite'?
I ask because I have never seen talk about this in my books, so is it maybe due to the informal definitions? or because it forces to add more mathematics than wanted into the book in order to be able to create such a proof? or because this is not the topic for introductory books? or for some other reason?
If $\Lambda$ is just some set which satisfies (1), (2), and (3), then "infinite" terms are not precluded. However, such definitions are intended to be inductive definitions which is the "additional assumption" Fabio Somenzi mentions. There are a variety of ways to formalize "inductive": initial algebras, least fixed points, minimality. In a set-theoretic context, the last is usually used. That is, we say for all sets $S$ which satisfy (1), (2), and (3), $\Lambda\subseteq S$ which is to say, $\Lambda$ is assumed to be the smallest set satisfying those constraints. It's clear a suitable set of finite terms is closed under rules (2) and (3) (and trivially for (1)) so $\Lambda$ doesn't include any infinite terms.