Dimension of image of a morphism ($\dim \overline{f(X)}=\dim X-\dim X_{\eta }$)

For an irreducible source, regard the morphism of algebraic varieties as dominant onto the closure of its image, with generic point $\eta$. The fiber dimension theorem gives the displayed formula. A proper morphism has closed image, so the closure can then be omitted.

Let $f:X\to Y$ be a proper morphism of irreducible algebraic varieties with equal dimension. If some fibre has an isolated point, its corresponding irreducible component has dimension zero. Apply the fiber dimension theorem to $X\to f(X)$: $0\ge \dim X-\dim f(X)$. Thus the closed image has dimension $\dim Y$ and equals $Y$. The incidence proof that a cubic surface contains a line is an application; the entire witness fibre need not be finite.