hasFDerivWithinAt_pi — Mathlib

English

If each coordinate map is differentiable, then the entire map into the product is differentiable.

Русский

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

LaTeX

$$$\\forall i, \\ Differentiable (Φ_i) x$ implies $\\ Differentiable Φ x$.$$

Lean4

theorem hasFDerivWithinAt_pi :
    HasFDerivWithinAt (fun x i => φ i x) (ContinuousLinearMap.pi φ') s x ↔ ∀ i, HasFDerivWithinAt (φ i) (φ' i) s x :=
  hasFDerivAtFilter_pi

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