contDiffAt_euclidean — Mathlib

English

Let f: H → ℝ^ι and y ∈ H. Then f is ContDiffAt of order n at y iff each coordinate function f_i is ContDiffAt of order n at y.

Русский

Пусть f: H → ℝ^ι и y ∈ H. Тогда f ∈ ContDiffAt^n в точке y эквивалентно тому, что каждая координата f_i гладна в точке y до порядка n.

LaTeX

$$$\\text{ContDiffAt}_{\\mathbb{k}}^{n} f\\ y \\iff \\forall i, \\text{ContDiffAt}_{\\mathbb{k}}^{n} (f_i)\\ y$$$

Lean4

theorem contDiffAt_euclidean {n : WithTop ℕ∞} : ContDiffAt 𝕜 n f y ↔ ∀ i, ContDiffAt 𝕜 n (fun x => f x i) y :=
  contDiffAt_piLp _

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