contDiffWithinAt_euclidean — Mathlib

English

Let f: H → ℝ^ι. Then f is ContDiffWithinAt of order n at y with respect to t if and only if each coordinate function f_i is ContDiffWithinAt of order n at y with respect to t.

Русский

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

LaTeX

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

Lean4

theorem contDiffWithinAt_euclidean {n : WithTop ℕ∞} :
    ContDiffWithinAt 𝕜 n f t y ↔ ∀ i, ContDiffWithinAt 𝕜 n (fun x => f x i) t y :=
  contDiffWithinAt_piLp _

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