writtenInExtChartAt_trivializationAt

English

When restricting to the trivialization, writing coordinates in extChartAt remains the identity on the fiber part.

Русский

При ограничении к тривиализации запись координат в extChartAt остаётся тождественной на волокне.

LaTeX

$$$$ writtenInExtChartAt (IB.prod 𝓘(𝕜, F)) (x) (trivializationAt F E x.proj) y = y $$$$

Lean4

theorem writtenInExtChartAt_trivializationAt {x : TotalSpace F E} {y}
    (hy : y ∈ (extChartAt (IB.prod 𝓘(𝕜, F)) x).target) :
    writtenInExtChartAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) x (trivializationAt F E x.proj) y = y :=
  writtenInExtChartAt_chartAt_comp _ hy

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