contDiff_iff_forall_nat_le — Mathlib

English

Let f be a map between normed spaces over 𝕜. Then f is C^n if and only if f is C^m for every natural m with m ≤ n. Equivalently, ContDiff 𝕜 n f holds exactly when ContDiff 𝕜 m f holds for all finite m ≤ n.

Русский

Пусть f: E → F — неравномерная функция между нормированными пространствами над 𝕜. Тогда f является C^n тогда и только тогда, когда она является C^m для каждого натурального m, удовлетворяющего m ≤ n.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{K}}(n)\ f \iff \forall m \in \mathbb{N}, \uparrow m \le n \ \Rightarrow \operatorname{ContDiff}_{\mathbb{K}}(m)\ f,$$$

Lean4

theorem contDiff_iff_forall_nat_le {n : ℕ∞} : ContDiff 𝕜 n f ↔ ∀ m : ℕ, ↑m ≤ n → ContDiff 𝕜 m f := by
  simp_rw [← contDiffOn_univ]; exact contDiffOn_iff_forall_nat_le

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