Manifold structure on the upper half plane. #
In this file we define the complex manifold structure on the upper half-plane.
The inclusion map ℍ → ℂ
is an analytic map of manifolds.
@[deprecated UpperHalfPlane.contMDiff_coe (since := "2024-11-20")]
Alias of UpperHalfPlane.contMDiff_coe
.
The inclusion map ℍ → ℂ
is an analytic map of manifolds.
The inclusion map ℍ → ℂ
is a differentiable map of manifolds.
theorem
UpperHalfPlane.contMDiffAt_ofComplex
{n : WithTop ℕ∞}
{z : ℂ}
(hz : 0 < z.im)
:
ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n (↑ofComplex) z
@[deprecated UpperHalfPlane.contMDiffAt_ofComplex (since := "2024-11-20")]
theorem
UpperHalfPlane.smoothAt_ofComplex
{n : WithTop ℕ∞}
{z : ℂ}
(hz : 0 < z.im)
:
ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n (↑ofComplex) z
Alias of UpperHalfPlane.contMDiffAt_ofComplex
.