English
Let I, I' define a smooth structure on M and M', and let f be a map with domain s ⊆ M and point x ∈ M. Then f is C^n within s at x iff f is C^m within s at x for every finite m ≤ n with m ≠ ∞.
Русский
Пусть задано гладкое отображение в смысле I, I' между многообразиями M и M'. Для f: M → M' и множества s ⊆ M, точка x ∈ M. Тогда ContMDiffWithinAt I I' n f s x эквивалентно ContMDiffWithinAt I I' m f s x для всех конечных m ≤ n, при условии m ≠ ∞.
LaTeX
$$$ ContMDiffWithinAt I I' n f s x \iff \forall m, m \le n \rightarrow m \neq \infty \rightarrow ContMDiffWithinAt I I' m f s x $$$
Lean4
/-- A function is `C^n` within a set at a point iff it is `C^m` within this set 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 contMDiffWithinAt_iff_le_ne_infty :
ContMDiffWithinAt I I' n f s x ↔ ∀ m, m ≤ n → m ≠ ∞ → ContMDiffWithinAt I I' m f s x :=
by
refine ⟨fun h m hm h'm ↦ h.of_le hm, fun h ↦ ?_⟩
cases n with
| top => exact h _ le_rfl (by simp)
| coe n => exact contMDiffWithinAt_iff_nat.2 (fun m hm ↦ h _ (mod_cast hm) (by simp))
