hasFDerivAt_apply — Mathlib

English

If each coordinate has strict differential, then the whole map has a strict differential.

Русский

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

LaTeX

$$$\\forall i, HasStrictFDerivAt (f_i) (f_i') x \\Rightarrow HasStrictFDerivAt Φ Φ' x.$$$

Lean4

@[fun_prop]
theorem hasFDerivAt_apply (i : ι) (f : ∀ i, F' i) : HasFDerivAt (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i) (proj i) f :=
  by
  apply HasStrictFDerivAt.hasFDerivAt
  apply hasStrictFDerivAt_apply

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