fdifferential_apply — Mathlib

English

Evaluating a ContMDiffMap at a point yields a linear map consistent with composition and evaluation.

Русский

Эвалюация ContMDiffMap в точке даёт линейное отображение, согласованное с композициями и эвалюацией.

LaTeX

$$$$ (\text{evalAt}_x) : C^∞⟮I,M; 𝕜⟯ → 𝕜 \,\text{is linear and compatible with evaluation.} $$$$

Lean4

@[simp]
theorem fdifferential_apply (f : C^∞⟮I, M; I', M'⟯) {x : M} (v : PointDerivation I x) (g : C^∞⟮I', M'; 𝕜⟯) :
    𝒅 f x v g = v (g.comp f) :=
  rfl

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