hfdifferential_apply — Mathlib

English

Evaluation at a point defines a linear functional on derivations by composing with evaluation.

Русский

Оценка в точке задаёт линейную функциональную карту на деривациях через композицию с эвалюацией.

LaTeX

$$$$ \mathrm{evalAt}_x: \ Derivation 𝕜 C^∞⟮I,M; 𝕜⟯ C^∞⟮I,M; 𝕜⟯ \to \ PointDerivation I x, \; v \mapsto v. $$$$

Lean4

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

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