fdifferential_comp

Mathlib.Geometry.Manifold.DerivationBundle

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

← MathLib Explorer

English

Applying the evaluation at x to a derivation yields the expected value on the function at x.

Русский

Применение оценки в x к деривации даёт ожидаемое значение функции в x.

LaTeX

$$$$ (\mathrm{evalAt}_x X) f = X f(x). $$$$

Lean4

@[simp]
theorem fdifferential_comp (g : C^∞⟮I', M'; I'', M''⟯) (f : C^∞⟮I, M; I', M'⟯) (x : M) :
    𝒅 (g.comp f) x = (𝒅 g (f x)).comp (𝒅 f x) :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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