contMDiff_smul — Mathlib

English

If hg > 0 for the determinant of g ∈ GL(2, ℝ), the action τ ↦ g · τ on the upper half-plane is ContMDiff of class n.

Русский

Если det(g) > 0 для g ∈ GL(2, ℝ), отображение τ ↦ g · τ на верхней полуплоскости является ContMDiff класса n.

LaTeX

$$$ContMDiff 𝓘(ℂ) 𝓘(ℂ) n (\lambda τ : ℍ, \; g \cdot τ)$$$

Lean4

/-- Each element of `GL(2, ℝ)⁺` defines a map of `C ^ n` manifolds `ℍ → ℍ`. -/
theorem contMDiff_smul {g : GL (Fin 2) ℝ} (hg : 0 < g.det.val) : ContMDiff 𝓘(ℂ) 𝓘(ℂ) n (fun τ : ℍ ↦ g • τ) := fun τ ↦
  by
  refine contMDiffAt_iff_target.mpr ⟨(continuous_const_smul g).continuousAt, ?_⟩
  simpa [glPos_smul_def hg] using (contMDiff_num g τ).mul (contMDiff_inv_denom g τ)

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