inCoordinates_tangent_bundle_core_model_space

English

The equivalence within ContMDiffWithinAt with model space reduces to ContDiffWithinAt for V on set s and x.

Русский

Лемма об эквивалентности внутри ContMDiffWithinAt сводится к ContDiffWithinAt для V на s и x.

LaTeX

$$$ContMDiffWithinAt_{I} (n, V, s, x) \iff ContDiffWithinAt_{\mathcal{I}}(n, V, s, x)$$$

Lean4

/-- The map `inCoordinates` for the tangent bundle is trivial on the model spaces -/
theorem inCoordinates_tangent_bundle_core_model_space (x₀ x : H) (y₀ y : H') (ϕ : E →L[𝕜] E') :
    inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ :=
  by
  erw [VectorBundleCore.inCoordinates_eq] <;> try trivial
  simp_rw [tangentBundleCore_indexAt, tangentBundleCore_coordChange_model_space, ContinuousLinearMap.id_comp,
    ContinuousLinearMap.comp_id]

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