contMDiff_coe — Mathlib

English

At points z ∈ ℂ with im(z) > 0, the map ofComplex is C^n differentiable from the upper-half-plane chart to the complex chart.

Русский

В точках z ∈ ℂ с Im(z) > 0 отображение ofComplex является C^n гладким между соответствующими диаграммами верхней полуплоскости и комплексной плоскости.

LaTeX

$$$\forall z \in \mathbb{C}, \operatorname{Im}(z) > 0 \Rightarrow \text{ContMDiffAt } 𝓘(\mathbb{C}) 𝓘(\mathbb{C}) n \text{ofComplex} \ z$$$

Lean4

/-- The inclusion map `ℍ → ℂ` is a map of `C^n` manifolds. -/
theorem contMDiff_coe : ContMDiff 𝓘(ℂ) 𝓘(ℂ) n ((↑) : ℍ → ℂ) := fun _ => contMDiffAt_extChartAt

Похожие утверждения