inTangentCoordinates_model_space — Mathlib

English

The model-space tangent coordinates are consistent with inCoordinates in the model-space context, yielding identity on model-space charts.

Русский

Координаты касательного пространства моделирования согласованы с inCoordinates в контексте моделирования пространства, давая тождество на диаграммах моделирования.

LaTeX

$$$inTangentCoordinates_model_space (f,g,\phi,x) = \phi$$$

Lean4

theorem inTangentCoordinates_model_space (f : N → H) (g : N → H') (ϕ : N → E →L[𝕜] E') (x₀ : N) :
    inTangentCoordinates I I' f g ϕ x₀ = ϕ := by
  simp +unfoldPartialApp only [inTangentCoordinates, inCoordinates_tangent_bundle_core_model_space]

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