pderivCLM_apply

Mathlib.Analysis.Distribution.SchwartzSpace

URI: https://scilib.ai/kg/mathlib#SchwartzMap.pderivCLM_apply

English

For m ∈ E and f ∈ 𝓢(E, F), pderivCLM 𝕜 m f = x ↦ D f(x)[m], i.e., the derivative in direction m.

Русский

Для m ∈ E и f ∈ 𝓢(E,F) имеем pderivCLM 𝕜 m f = x ↦ D f(x)[m], то есть производная в направлении m.

LaTeX

$$$pderivCLM 𝕜\, m\, f = f'(\cdot)\cdot m$$$

Lean4

@[simp]
theorem pderivCLM_apply (m : E) (f : 𝓢(E, F)) (x : E) : pderivCLM 𝕜 m f x = fderiv ℝ f x m :=
  rfl

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

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

Разделы

Аффилиация

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