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 : ChartedSpace ℂ UpperHalfPlane

instance UpperHalfPlane.instSmoothManifoldWithCornersComplexToNontriviallyNormedFieldInstDenselyNormedFieldComplexInstNormedAddCommGroupComplexToNormedSpaceToNormedFieldToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfUpperHalfPlaneInstTopologicalSpaceUpperHalfPlaneInstChartedSpaceComplexToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplexUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : SmoothManifoldWithCorners (modelWithCornersSelf ℂ ℂ) UpperHalfPlane

theorem UpperHalfPlane.smooth_coe : Smooth (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) UpperHalfPlane.coe

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

theorem UpperHalfPlane.mdifferentiable_coe : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) UpperHalfPlane.coe

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