continuousLinearMapAt_trivializationAt

English

The constant map on a set is ContMDiffOn.

Русский

Постоянное отображение на множестве гладко.

LaTeX

$$$$ \ContMDiffOn I I' n (\lambda x, c)\, s $$$$

Lean4

/-- The trivialization of the tangent bundle at a point is the manifold derivative of the
extended chart.
Use with care as this abuses the defeq `TangentSpace 𝓘(𝕜, E) y = E` for `y : E`. -/
theorem continuousLinearMapAt_trivializationAt {x₀ x : M} (hx : x ∈ (chartAt H x₀).source) :
    (trivializationAt E (TangentSpace I) x₀).continuousLinearMapAt 𝕜 x = mfderiv I 𝓘(𝕜, E) (extChartAt I x₀) x :=
  by
  have : MDifferentiableAt I 𝓘(𝕜, E) (extChartAt I x₀) x := mdifferentiableAt_extChartAt hx
  simp only [extChartAt, OpenPartialHomeomorph.extend, PartialEquiv.coe_trans, ModelWithCorners.toPartialEquiv_coe,
    OpenPartialHomeomorph.toFun_eq_coe] at this
  simp [hx, mfderiv, this]

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