English
For a fixed natural number n, ContDiffWithinAt 𝕜 n f s x is characterized by the existence of a neighborhood u around x contained in s and a formal multilinear Taylor series p with HasFTaylorSeriesUpToOn n f p u.
Русский
Для данного натурального числа n ContDiffWithinAt 𝕜 n f s x эквивалентно существованию окрестности u вокруг x, содержащейся в s, и формальной многошкальной серии Тейлора p such that HasFTaylorSeriesUpToOn n f p u.
LaTeX
$$$ ContDiffWithinAt 𝕜 n f s x \\iff \\exists u \\in 𝓝[insert x s] x, \\; \\exists p : E \\to \\text{FormalMultilinearSeries } 𝕜 E F,\\ HasFTaylorSeriesUpToOn n f p u$$
Lean4
theorem contDiffWithinAt_nat {n : ℕ} :
ContDiffWithinAt 𝕜 n f s x ↔
∃ u ∈ 𝓝[insert x s] x, ∃ p : E → FormalMultilinearSeries 𝕜 E F, HasFTaylorSeriesUpToOn n f p u :=
⟨fun H => H n le_rfl, fun ⟨u, hu, p, hp⟩ _m hm => ⟨u, hu, p, hp.of_le (mod_cast hm)⟩⟩
