contMDiff_num — Mathlib

English

For every g in GL(2, ℝ), the map τ ↦ num(g, τ) is continuously differentiable of class n with respect to the complex structure on the upper half-plane.

Русский

Для каждого g ∈ GL(2, ℝ) отображение τ ↦ num(g, τ) является ContMDiff класса n по комплексной структуре на верхней полуплоскости.

LaTeX

$$$ContMDiff 𝓘(ℂ) 𝓘(ℂ) n (τ \mapsto \mathrm{num}(g, τ))$$$

Lean4

theorem contMDiff_num (g : GL (Fin 2) ℝ) : ContMDiff 𝓘(ℂ) 𝓘(ℂ) n (fun τ : ℍ ↦ num g τ) :=
  (contMDiff_const.smul contMDiff_coe).add contMDiff_const

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