continuousLinearMapAt_model_space

English

Instance: if I is a manifold with ω-nature on M, then ContMDiffVectorBundle ω E TangentSpace I I holds.

Русский

Экземпляр: если I является многообразием с ω-структурой на M, то ContMDiffVectorBundle ω E TangentSpace I I выполняется.

LaTeX

$$ContMDiffVectorBundle ω E (TangentSpace I) I$$

Lean4

@[simp high, mfld_simps]
theorem continuousLinearMapAt_model_space (b b' : F) :
    (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b).continuousLinearMapAt 𝕜 b' = (1 : F →L[𝕜] F) :=
  by
  rw [TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, coordChange_model_space]
  apply mem_univ

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