writtenInExtChartAt_trivializationAt_symm

English

The target of extChartAt equals a product with universal fiber component, reflecting the fibre-bundle structure.

Русский

Цель ExtChartAt является произведением с универсальным волокновым компонентом, отражая структуру пучка.

LaTeX

$$$$ (extChartAt (IB.prod 𝓘(𝕜, F)) x).target = (extChartAt IB x.proj).target \\times univ $$$$

Lean4

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

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