iteratedFDeriv_zero_apply

Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

URI: https://scilib.ai/kg/mathlib#iteratedFDeriv_zero_apply

English

For m : Fin 0 → E, (iteratedFDeriv 𝕜 0 f x) m = f x.

Русский

Для единственного элемента в Fin 0 производная нулевого порядка совпадает с f(x).

LaTeX

$$$(\operatorname{iteratedFDeriv}_{\mathbb{K}}^{0} f x)(m) = f x$$$

Lean4

@[simp]
theorem iteratedFDeriv_zero_apply (m : Fin 0 → E) : (iteratedFDeriv 𝕜 0 f x : (Fin 0 → E) → F) m = f x :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru