English
A function is C^n at a point within a set, for ENat n, iff it is C^m at that point within the set for every m with m ≤ n and m ≠ ∞.
Русский
Функция в точке внутри множества является C^n, если и только если она является C^m в той же точке внутри множества для каждого m, удовлетворяющего m ≤ n и m ≠ ∞.
LaTeX
$$$ ContMDiffWithinAt I I' n f s x \iff \forall m, m \le n \rightarrow m \neq ∞ \rightarrow ContMDiffWithinAt I I' m f s x $$$
Lean4
/-- A function is `C^n`at a point iff it is `C^m`at this point, for
any `m ≤ n` which is different from `∞`. This result is useful because, when `m ≠ ∞`, being
`C^m` extends locally to a neighborhood, giving flexibility for local proofs. -/
theorem contMDiffAt_iff_le_ne_infty : ContMDiffAt I I' n f x ↔ ∀ m, m ≤ n → m ≠ ∞ → ContMDiffAt I I' m f x :=
by
simp only [← contMDiffWithinAt_univ]
rw [contMDiffWithinAt_iff_le_ne_infty]
