fderiv — Mathlib

English

If a function is polynomial on a set, so is its Fréchet derivative.

Русский

Если функция полиномальна на множестве, то и ее производная по Фреше тоже полиномальна на этом множестве.

LaTeX

$$$\text{CPolynomialOn } 𝕜 f s \Rightarrow \text{CPolynomialOn } 𝕜 (fderiv 𝕜 f) s$$$

Lean4

/-- If a function is polynomial on a set `s`, so is its Fréchet derivative. -/
theorem fderiv (h : CPolynomialOn 𝕜 f s) : CPolynomialOn 𝕜 (fderiv 𝕜 f) s :=
  by
  intro y hy
  rcases h y hy with ⟨p, r, n, hp⟩
  exact hp.fderiv'.cpolynomialAt

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