differentiable_qParam — Mathlib

English

For every real h, the map z ↦ qParam(h, z) is differentiable with respect to z in the complex plane.

Русский

Для каждого действительного h отображение z ↦ qParam(h, z) дифференцируемо по z в комплексной плоскости.

LaTeX

$$$\forall h \in \mathbb{R},\; \text{Differentiable}_{\mathbb{C}}(z \mapsto qParam(h,z))$$$

Lean4

@[fun_prop]
theorem differentiable_qParam : Differentiable ℂ (𝕢 h) :=
  by
  unfold qParam
  fun_prop

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