iteratedFDerivWithin_succ_const — Mathlib

English

Constants are infinitely differentiable; the zero function is smooth of all orders.

Русский

Константы бесконечно дифференцируемы; нулевая функция гладна по всем порядкам.

LaTeX

$$$ContDiff 𝕜 n (\\lambda x. c)$ и $ContDiff 𝕜 n (\\lambda x. 0)$ для любого c, n$$

Lean4

theorem iteratedFDerivWithin_succ_const (n : ℕ) (c : F) : iteratedFDerivWithin 𝕜 (n + 1) (fun _ : E ↦ c) s = 0 := by
  induction n with
  | zero =>
    ext1
    simp [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp, comp_def]
  | succ n IH =>
    rw [iteratedFDerivWithin_succ_eq_comp_left, IH]
    simp only [Pi.zero_def, comp_def, fderivWithin_fun_const, map_zero]

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