differentiableOn_euclidean — Mathlib

English

A map f: H → EuclideanSpace is differentiable on a set t iff each coordinate map f_i is differentiable on t.

Русский

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

LaTeX

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

Lean4

theorem differentiableOn_euclidean : DifferentiableOn 𝕜 f t ↔ ∀ i, DifferentiableOn 𝕜 (fun x => f x i) t :=
  differentiableOn_piLp _

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