fderivWithin — Mathlib

English

If a function is analytic on a set, then its derivative within that set is analytic on the same set.

Русский

Если функция аналитична на множестве, то её производная внутри множества аналитична на том же множестве.

LaTeX

$$$\\text{AnalyticOn } f s \\Rightarrow \\text{AnalyticOn } (fderivWithin 𝕜 f s) s$$$

Lean4

/-- If a function is analytic within a set with unique differentials, then so is its derivative.
Note that this theorem does not require completeness of the space. -/
protected theorem fderivWithin (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) : AnalyticOn 𝕜 (fderivWithin 𝕜 f s) s :=
  by
  intro x hx
  rcases h x hx with ⟨p, r, hr⟩
  refine ⟨p.derivSeries, r, hr.fderivWithin_of_mem_of_analyticOn h hu hx⟩

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