differentiableAt_euclidean — Mathlib

English

A map f: H → EuclideanSpace is differentiable at y iff each coordinate map f_i is differentiable at y.

Русский

Отображение f: H → EuclideanSpace дифференцируемо в точке y тогда и только тогда, когда каждая координатная функция f_i дифференцируема в y.

LaTeX

$$$\text{DifferentiableAt}_{\mathbb{K}}(f,y) \iff \forall i, \text{DifferentiableAt}_{\mathbb{K}}(\lambda x. f(x)_i,y).$$$

Lean4

theorem differentiableAt_euclidean : DifferentiableAt 𝕜 f y ↔ ∀ i, DifferentiableAt 𝕜 (fun x => f x i) y :=
  differentiableAt_piLp _

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