continuousOn_tangentCoordChange — Mathlib

English

There is a natural topology on the tangent bundle TM induced by the tangent bundle core.

Русский

ТangentBundle(TM) имеет естественную топологию, индуцированную ядром касательного расслоения.

LaTeX

$$$$ \operatorname{TopologicalSpace}(TM) = (\text{tangentBundleCore } I M).toTopologicalSpace $$$$

Lean4

theorem continuousOn_tangentCoordChange (x y : M) :
    ContinuousOn (tangentCoordChange I x y) ((extChartAt I x).source ∩ (extChartAt I y).source) := by
  convert (tangentBundleCore I M).continuousOn_coordChange (achart H x) (achart H y) <;>
    simp only [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]

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