deriv_pi — Mathlib

English

If each coordinate φ x i is differentiable at x, then deriv φ x equals the Pi of coordinate derivatives.

Русский

Если каждая координата φ x i дифференцируема в x, то deriv φ x равняется Pi-образу координатных производных.

LaTeX

$$$\text{deriv }\phi x = \lambda i. \text{deriv } (\lambda x. \phi x i) x$$$

Lean4

theorem deriv_pi (h : ∀ i, DifferentiableAt 𝕜 (fun x => φ x i) x) : deriv φ x = fun i => deriv (fun x => φ x i) x :=
  (hasDerivAt_pi.2 fun i => (h i).hasDerivAt).deriv

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