English
Let M be a manifold over a field 𝕜 and x a point of M. For any ENat n and a map f: M → M, f is C^n at x iff f is C^m at x for every natural m with m ≤ n. Equivalently, the C^n regularity at a point is the conjunction of all finite C^m regularities up to n.
Русский
Пусть M — многообразие над полем 𝕜, и возьмем точку x ∈ M. Пусть n ∈ ENat. Тогда функция f: M → M удовлетворяет: f C^n в x тогда и только если для каждого натурального m ≤ n функция f является C^m в x. Иными словами, C^n-гладкость в точке эквивалентна существованию всех конечных уровней гладкости до n.
LaTeX
$$$ ContMDiffAt I I' n f x \Longleftrightarrow \forall m \in \mathbb{N}, (m \le n) \Rightarrow ContMDiffAt I I' m f x $$$
Lean4
theorem contMDiffAt_iff_nat {n : ℕ∞} : ContMDiffAt I I' n f x ↔ ∀ m : ℕ, (m : ℕ∞) ≤ n → ContMDiffAt I I' m f x := by
simp [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_nat]
