mathlib3 documentation


Manifold structure on the upper half plane. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define the complex manifold structure on the upper half-plane.

The inclusion map ℍ → ℂ is a smooth map of manifolds.

The inclusion map ℍ → ℂ is a differentiable map of manifolds.