The logarithm maps the upper half-plane onto a strip

The principal logarithm is a holomorphic bijection from the open upper half-plane onto the horizontal strip with imaginary part between 0 and π. Its inverse is complex exponentiation. This supplies the logarithmic coordinate for parallel-sided conformal ends.

theorem TauCeti.bijOn_log_upperHalfPlaneSet : Set.BijOn Complex.log UpperHalfPlane.upperHalfPlaneSet {w : ℂ | w.im ∈ Set.Ioo 0 Real.pi}

The principal logarithm maps the upper half-plane bijectively onto the open horizontal strip of height π.