differentiable_euclidean — Mathlib

English

A map f: H → EuclideanSpace is differentiable iff all its coordinate maps are differentiable.

Русский

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

LaTeX

$$$\text{Differentiable}_{\mathbb{K}}(f) \iff \forall i, \text{Differentiable}_{\mathbb{K}}(x \mapsto f(x)_i).$$$

Lean4

theorem differentiable_euclidean : Differentiable 𝕜 f ↔ ∀ i, Differentiable 𝕜 fun x => f x i :=
  differentiable_piLp _

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