trivializationAt_continuousLinearMapAt

English

For trivializations at b₀, if b lies in their base set, the continuous linear map equals coordChange between the corresponding indices.

Русский

Для тривиализаций в точке b₀, если b лежит в их базовом множестве, непрерывное линейное отображение равно coordChange между соответствующими индексами.

LaTeX

$$trivializationAt_continuousLinearMapAt: hb ⇒ (Z.localTriv i).continuousLinearMapAt R b = Z.coordChange (Z.indexAt b) i b$$

Lean4

@[simp, mfld_simps]
theorem trivializationAt_continuousLinearMapAt {b₀ b : B} (hb : b ∈ (trivializationAt F Z.Fiber b₀).baseSet) :
    (trivializationAt F Z.Fiber b₀).continuousLinearMapAt R b = Z.coordChange (Z.indexAt b) (Z.indexAt b₀) b :=
  Z.localTriv_continuousLinearMapAt hb

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