evalAt_apply

Mathlib.Geometry.Manifold.DerivationBundle

URI: https://scilib.ai/kg/mathlib#Derivation.evalAt_apply

English

Evaluation at x yields a linear map from ContMDiffMap to 𝕜 by evaluating the function at x in the target model.

Русский

Эвалюация в x даёт линейное отображение от ContMDiffMap в 𝕜 через значение функции в x.

LaTeX

$$$$ \text{evalAt}(x) : C^∞⟮I,M;\mathbb{K}\⟯ \to \mathbb{K}, \; f \mapsto f(x). $$$$

Lean4

theorem evalAt_apply (x : M) : evalAt x X f = (X f) x :=
  rfl

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

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

Разделы

Аффилиация

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