English
Let D be a finite-dimensional normed space over 𝕜 and s a subset with UniqueDiffOn 𝕜 s. Then ContDiffOn 𝕜 (n+1) f s holds if and only if f is differentiable on s, and if n = ω then f is analytic on s, and for every y ∈ D the map x ↦ fderivWithin 𝕜 f s x y is ContDiffOn 𝕜 n on s.
Русский
Пусть D — конечномерное нормированное пространство над 𝕜, s — подмножество с уникальной дифференцируемостью 𝕜; тогда ContDiffOn 𝕜 (n+1) f s эквивалентно тому, что f дифференцируема на s, и если n = ω, то f аналитична на s, и для любого y ∈ D отображение x ↦ fderivWithin 𝕜 f s x y принадлежит ContDiffOn 𝕜 n на s.
LaTeX
$$$ ContDiffOn 𝕜 (n+1) f s \ \Longleftrightarrow\ \Big( \text{DifferentiableOn } 𝕜 f s \Big) \land \Big( (n = \omega) \rightarrow AnalyticOn 𝕜 f s \Big) \land \forall y,\ ContDiffOn 𝕜 n (\lambda x. fderivWithin 𝕜 f s x y) s $$$
Lean4
theorem contDiffOn_succ_iff_fderiv_apply [FiniteDimensional 𝕜 D] (hs : UniqueDiffOn 𝕜 s) :
ContDiffOn 𝕜 (n + 1) f s ↔
DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ∀ y, ContDiffOn 𝕜 n (fun x => fderivWithin 𝕜 f s x y) s :=
by rw [contDiffOn_succ_iff_fderivWithin hs, contDiffOn_clm_apply]
