contDiffOn — Mathlib

English

A polynomial is smooth of all orders on any subset.

Русский

Полином гладок по всем порядкам на любом подмножестве.

LaTeX

$$$\displaystyle \text{contDiffOn (h : CPolynomialOn 𝕜 f s) }\; {n} : \ ContDiffOn 𝕜 n f s$$$

Lean4

/-- A polynomial function is infinitely differentiable. -/
theorem contDiffOn (h : CPolynomialOn 𝕜 f s) {n : WithTop ℕ∞} : ContDiffOn 𝕜 n f s :=
  by
  let t := {x | CPolynomialAt 𝕜 f x}
  suffices ContDiffOn 𝕜 n f t from this.mono h
  suffices AnalyticOnNhd 𝕜 f t by
    have t_open : IsOpen t := isOpen_cpolynomialAt 𝕜 f
    exact AnalyticOnNhd.contDiffOn this t_open.uniqueDiffOn
  have H : CPolynomialOn 𝕜 f t := fun _x hx ↦ hx
  exact H.analyticOnNhd

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