contDiffAt — Mathlib

English

If f is analytic at a point and the space is complete, then ContDiffAt holds.

Русский

Если f аналитична в точке и пространство полное, то ContDiffAt выполняется.

LaTeX

$$$\\text{AnalyticAt 𝕜 f x} \\land \\text{CompleteSpace } F \\Rightarrow \\ContDiffAt 𝕜 n f x$$$

Lean4

/-- In a complete space, a function which is analytic at a point is also `C^ω` there.
Note that the same statement for `AnalyticOn` does not require completeness, see
`AnalyticOn.contDiffOn`. -/
theorem contDiffAt [CompleteSpace F] (h : AnalyticAt 𝕜 f x) : ContDiffAt 𝕜 n f x :=
  by
  rw [← contDiffWithinAt_univ]
  rw [← analyticWithinAt_univ] at h
  exact h.contDiffWithinAt

Похожие утверждения