differentiableAt_pi — Mathlib

English

If every coordinate is differentiable, then the product map is differentiable (strong form).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem differentiableAt_pi : DifferentiableAt 𝕜 Φ x ↔ ∀ i, DifferentiableAt 𝕜 (fun x => Φ x i) x :=
  ⟨fun h i => (hasFDerivAt_pi'.1 h.hasFDerivAt i).differentiableAt, fun h =>
    (hasFDerivAt_pi.2 fun i => (h i).hasFDerivAt).differentiableAt⟩

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