mathlib3 documentation

analysis.complex.upper_half_plane.manifold

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.

source
@[protected, instance]
noncomputable def upper_half_plane.charted_space  :
charted_space ℂ upper_half_plane
Equations
source
@[protected, instance]
def upper_half_plane.smooth_manifold_with_corners  :
smooth_manifold_with_corners (model_with_corners_self ℂ ℂ) upper_half_plane
source
theorem upper_half_plane.smooth_coe  :
smooth (model_with_corners_self ℂ ℂ) (model_with_corners_self ℂ ℂ) coe

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

source
theorem upper_half_plane.mdifferentiable_coe  :
mdifferentiable (model_with_corners_self ℂ ℂ) (model_with_corners_self ℂ ℂ) coe

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