differentiableWithinAt_pi'' — Mathlib

English

If Φ is differentiable with derivative Φ′, then each coordinate Φ_i is differentiable with derivative Φ′_i.

Русский

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

LaTeX

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

Lean4

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

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