contDiffOn_euclidean — Mathlib

English

Let f: H → ℝ^ι and t ⊆ H. Then f is ContDiffOn of order n on t iff each coordinate function f_i is ContDiffOn of order n on t.

Русский

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

LaTeX

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

Lean4

theorem contDiffOn_euclidean {n : WithTop ℕ∞} : ContDiffOn 𝕜 n f t ↔ ∀ i, ContDiffOn 𝕜 n (fun x => f x i) t :=
  contDiffOn_piLp _

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