UpperHalfPlane.continuous_coe

theorem UpperHalfPlane.continuous_coe : Continuous UpperHalfPlane.coe

This theorem states that the canonical embedding of the upper half-plane into the complex numbers, denoted as `UpperHalfPlane.coe`, is continuous. In other words, it guarantees that for every point in the upper half-plane, small changes in the input result in small changes in the output when mapped to the complex numbers using the function `UpperHalfPlane.coe`. This is a fundamental requirement in topology and complex analysis.

More concisely: The function `UpperHalfPlane.coe` mapping the upper half-plane to the complex numbers is continuous.