Theorem on formal functions

In algebraic geometry, the theorem on formal functions states the following:

The theorem is used to deduce some other important theorems: Stein factorization and a version of Zariski's main theorem that says that a proper birational morphism into a normal variety is an isomorphism. Some other corollaries (with the notations as above) are:

Corollary: For any ${\displaystyle s\in S}$, topologically,

where the completion on the left is with respect to ${\displaystyle {\mathfrak {m}}_{s}}$.

Corollary: Let r be such that ${\displaystyle \operatorname {dim} f^{-1}(s)\leq r}$ for all ${\displaystyle s\in S}$. Then

Corollay: For each ${\displaystyle s\in S}$, there exists an open neighborhood U of s such that

Corollary: If ${\displaystyle f_{*}{\mathcal {O}}_{X}={\mathcal {O}}_{S}}$, then ${\displaystyle f^{-1}(s)}$ is connected for all ${\displaystyle s\in S}$.

The theorem also leads to the Grothendieck existence theorem, which gives an equivalence between the category of coherent sheaves on a scheme and the category of coherent sheaves on its formal completion (in particular, it yields algebralizability.)