differentiableWithinAt_euclidean — Mathlib

English

A function into a finite-dimensional Euclidean space is differentiable at a point iff each coordinate function is differentiable at that point.

Русский

Функция из пространства в конечномерное Евклидово пространство дифференцируема в точке тогда и только тогда, когда каждая координатная функция дифференцируема в этой точке.

LaTeX

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

Lean4

theorem differentiableWithinAt_euclidean :
    DifferentiableWithinAt 𝕜 f t y ↔ ∀ i, DifferentiableWithinAt 𝕜 (fun x => f x i) t y :=
  differentiableWithinAt_piLp _

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