Dimension of image of a morphism (source code)

= Dimension of image of a morphism
{title2=$\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.