differentiable_pi — Mathlib

English

If Φ is differentiable and coordinatewise differentiable, then the composed map Φ is differentiable with the composition of the coordinate derivatives.

Русский

Если Φ дифференцируема и координатно дифференцируема, тогда составная Φ дифференцируема с производными координат.

LaTeX

$$$\\text{Differentiable } Φ \\Rightarrow \\forall i, \\text{Differentiable } Φ_i.$$$

Lean4

theorem differentiable_pi : Differentiable 𝕜 Φ ↔ ∀ i, Differentiable 𝕜 fun x => Φ x i :=
  ⟨fun h i x => differentiableAt_pi.1 (h x) i, fun h x => differentiableAt_pi.2 fun i => h i x⟩

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