mdifferentiableAt_ofComplex — Mathlib

English

For z ∈ ℂ with Im(z) > 0, the map UpperHalfPlane.ofComplex is MDifferentiable at z when viewed as a chart map.

Русский

Для z ∈ ℂ с Im(z) > 0 отображение UpperHalfPlane.ofComplex гладко в точке z как отображение карты диаграммы.

LaTeX

$$$\forall z \in \mathbb{C}, \operatorname{Im}(z) > 0 \Rightarrow \text{MDifferentiableAt } \text{modelWithCornersSelf Complex Complex} \text{ UpperHalfPlane.ofComplex.toFun'} z$$$

Lean4

theorem mdifferentiableAt_ofComplex {z : ℂ} (hz : 0 < z.im) : MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) ofComplex z :=
  (contMDiffAt_ofComplex hz).mdifferentiableAt le_top

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