mdifferentiable_inv_denom — Mathlib

English

For every g ∈ GL(2, ℝ), the map τ ↦ denom(g, τ)^{-1} is MDifferentiable with the model with corners and Complex structure.

Русский

Для каждого g ∈ GL(2, ℝ) отображение τ ↦ denom(g, τ)^{-1} MD-дифференцируемо на модели с краями и комплексной структурой.

LaTeX

$$$MDifferentiable (modelWithCornersSelf \mathbb{C} \mathbb{C}) (modelWithCornersSelf \mathbb{C} \mathbb{C}) (\lambda τ, \; \mathrm{denom}(g, τ)^{-1})$$$

Lean4

theorem mdifferentiable_inv_denom (g : GL (Fin 2) ℝ) : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (fun τ : ℍ ↦ (denom g τ)⁻¹) :=
  (contMDiff_inv_denom g).mdifferentiable le_top

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