eval_germ — Mathlib

English

The trivialization of the tangent bundle matches the MFDeriv of the extended chart.

Русский

Тривиализация касательной фибры совпадает с MF-дифференциалом расширенного чарта.

LaTeX

$$$$ (trivializationAt E (TangentSpace I) x_0).continuousLinearMapAt 𝕜 x = \mathrm{mfderiv} I \mathcal{I}(\mathfrak{k}, E) (extChartAt I x_0) x $$$$

Lean4

@[simp]
theorem eval_germ (U : Opens M) (x : M) (hx : x ∈ U) (f : (smoothSheaf IM I M N).presheaf.obj (op U)) :
    smoothSheaf.eval IM I N (x : M) ((smoothSheaf IM I M N).presheaf.germ U x hx f) = f ⟨x, hx⟩ :=
  TopCat.stalkToFiber_germ ((contDiffWithinAt_localInvariantProp ∞).localPredicate M N) _ _ _ _

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