English
Let Z be a VectorBundleCore over a base B, with fiber F. For any b0, b1, b in B such that b lies in the intersection of the base sets of the trivializations at b0 and b1, and for any v in F, the fiberwise coordinate-change between the trivializations equals the core's coordinate change: coordChangeL between b0 and b1 applied to b and v equals Z.coordChange at (indexAt b0, indexAt b1) applied to b and v.
Русский
Пусть Z - VectorBundleCore над базой B с волокном F. Для любых b0, b1, b в B such что b лежит в пересечении базовых множеств тривиализаций в b0 и b1, и для любого v ∈ F, переход координат между тривиализациями равен переходу, заданному Z.coordChange: coordChangeL между b0 и b1, применяемое к b и v, равно Z.coordChange (indexAt b0) (indexAt b1) b v.
LaTeX
$$$\\\\forall b_0,b_1,b \\,\\\\in B, \\\\ hb \\\\in (\\\\operatorname{trivializationAt} F Z.Fiber b_0).baseSet \\\\cap (\\\\operatorname{trivializationAt} F Z.Fiber b_1).baseSet, \\\\forall v \\\\in F:\\\\ (\\\\operatorname{trivializationAt} F Z.Fiber b_0).coordChangeL R (\\\\operatorname{trivializationAt F Z.Fiber b_1}) b v = Z.coordChange (Z.indexAt b_0) (Z.indexAt b_1) b v. $$$$
Lean4
@[simp, mfld_simps]
theorem trivializationAt_coordChange_eq {b₀ b₁ b : B}
(hb : b ∈ (trivializationAt F Z.Fiber b₀).baseSet ∩ (trivializationAt F Z.Fiber b₁).baseSet) (v : F) :
(trivializationAt F Z.Fiber b₀).coordChangeL R (trivializationAt F Z.Fiber b₁) b v =
Z.coordChange (Z.indexAt b₀) (Z.indexAt b₁) b v :=
Z.localTriv_coordChange_eq _ _ hb v
