mdifferentiable_num — Mathlib

English

For every g ∈ GL(2, ℝ), the map τ ↦ num(g, τ) is MDifferentiable on the model with corners with Complex structure.

Русский

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

LaTeX

$$$MDifferentiable (modelWithCornersSelf \mathbb{C} \mathbb{C}) (\text{modelWithCornersSelf } \mathbb{C} \mathbb{C}) (f \mapsto \mathrm{num}(g, f))$$$

Lean4

theorem mdifferentiable_num (g : GL (Fin 2) ℝ) : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (fun τ : ℍ ↦ num g τ) :=
  (contMDiff_num g).mdifferentiable le_top

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