differentiableAt_pi'' — Mathlib

English

If Φ is differentiable at x with coordinates differentiable, then Φ is differentiable at x.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem differentiableAt_pi'' (hφ : ∀ i, DifferentiableAt 𝕜 (fun x => Φ x i) x) : DifferentiableAt 𝕜 Φ x :=
  differentiableAt_pi.2 hφ

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