English
Rewrite of inCoordinates with an explicit equality in terms of composition with trivializations and coordinate changes.
Русский
Переписывание inCoordinates через композицию с тривиализации и переходами координат.
LaTeX
$$$$ inCoordinates F E F' E' x_0 x y_0 y ϕ = (trivializationAt F' E' y_0).continuousLinearMapAt 𝕜_2 y).comp (ϕ.comp (trivializationAt F E x_0).symmL 𝕜_1 x) $$$$
Lean4
/-- Rewrite `ContinuousLinearMap.inCoordinates` in a `VectorBundleCore`. -/
protected theorem _root_.VectorBundleCore.inCoordinates_eq {ι ι'} (Z : VectorBundleCore 𝕜₁ B F ι)
(Z' : VectorBundleCore 𝕜₂ B' F' ι') {x₀ x : B} {y₀ y : B'} (ϕ : F →SL[σ] F') (hx : x ∈ Z.baseSet (Z.indexAt x₀))
(hy : y ∈ Z'.baseSet (Z'.indexAt y₀)) :
inCoordinates F Z.Fiber F' Z'.Fiber x₀ x y₀ y ϕ =
(Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y).comp (ϕ.comp <| Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x) :=
by simp_rw [inCoordinates, Z'.trivializationAt_continuousLinearMapAt hy, Z.trivializationAt_symmL hx]
