UpperHalfPlane.mdifferentiable_coe
theorem UpperHalfPlane.mdifferentiable_coe :
MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) UpperHalfPlane.coe
This theorem states that the inclusion map from the upper half-plane `ℍ` into the complex numbers `ℂ` is a differentiable map of manifolds. That is, the function that embeds the upper half-plane into the complex plane (represented by the function `UpperHalfPlane.coe`) is smoothly differentiable. The spaces of the upper half-plane and the complex plane are both modeled on the same vector space (the complex numbers), as indicated by the `modelWithCornersSelf ℂ ℂ` arguments.
More concisely: The inclusion map from the upper half-plane to the complex numbers is a smoothly differentiable manifold homomorphism.
|
UpperHalfPlane.smooth_coe
theorem UpperHalfPlane.smooth_coe : Smooth (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) UpperHalfPlane.coe
This theorem states that the inclusion map from the upper half-plane (denoted as ℍ) to the complex numbers (ℂ), represented by the function `UpperHalfPlane.coe`, is a 'smooth' map of manifolds. In mathematical terms, 'smoothness' of a function implies that it has derivatives of all orders at every point, and in the context of manifolds, this property is preserved under transitions between different coordinate systems. The 'modelWithCornersSelf' function denotes a specific kind of mathematical structure (a model with corners) used in the formalism of differential geometry. Specifically, it is constructed to be a model with corners on the field of complex numbers with itself as the model space.
More concisely: The inclusion map from the upper half-plane to the complex numbers is a smooth function as manifolds.
|