ThmDex – An index of mathematical definitions, results, and conjectures.
Result R3472 on D1392: Holomorphic function
Maximum modulus principle
Formulation 0
Let $\Omega \subseteq \mathbb{C}$ be a D4898: Complex domain such that
(i) \begin{equation} \Omega \neq \emptyset \end{equation}
(ii) $f : \Omega \to \mathbb{C}$ is a D1392: Holomorphic function on $\Omega$
(iii) \begin{equation} \exists \, z, w \in \Omega : z \neq w \text{ and } f(z) \neq f(w) \end{equation}
Then \begin{equation} \max_{z \in \Omega} |f(z)| = \emptyset \end{equation}
Proofs
Proof 0
Let $\Omega \subseteq \mathbb{C}$ be a D4898: Complex domain such that
(i) \begin{equation} \Omega \neq \emptyset \end{equation}
(ii) $f : \Omega \to \mathbb{C}$ is a D1392: Holomorphic function on $\Omega$
(iii) \begin{equation} \exists \, z, w \in \Omega : z \neq w \text{ and } f(z) \neq f(w) \end{equation}
With these assumptions, result R3471: Open complex mapping theorem shows that $f$ is an open function; hence the image $f(\Omega)$ is open in $\mathbb{C}$. Now the claim is a consequence of the result R3473: Euclidean real function with open image set does not attain maximum. $\square$