Manifold structure on the upper half plane. #
In this file we define the complex manifold structure on the upper half-plane.
noncomputable instance
UpperHalfPlane.instChartedSpaceComplexToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplexUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane :
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The inclusion map ℍ → ℂ
is a smooth map of manifolds.
The inclusion map ℍ → ℂ
is a differentiable map of manifolds.