case h
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.380014
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_4
Z : VectorBundleCore R B F ι
i j k : ι
x : B
hx : x ∈ baseSet Z i ∩ baseSet Z j ∩ baseSet Z k
v : F
⊢ ↑(ContinuousLinearMap.comp (coordChange Z j k x) (coordChange Z i j x)) v = ↑(coordChange Z i k x) v
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.380014
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_4
Z : VectorBundleCore R B F ι
i j k : ι
x : B
hx : x ∈ baseSet Z i ∩ baseSet Z j ∩ baseSet Z k
⊢ ContinuousLinearMap.comp (coordChange Z j k x) (coordChange Z i j x) = coordChange Z i k x
ext v
no goals
case h
R : Type u_2
B : Type u_1
F : Type u_3
E : B → Type ?u.380014
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_4
Z : VectorBundleCore R B F ι
i j k : ι
x : B
hx : x ∈ baseSet Z i ∩ baseSet Z j ∩ baseSet Z k
v : F
⊢ ↑(ContinuousLinearMap.comp (coordChange Z j k x) (coordChange Z i j x)) v = ↑(coordChange Z i k x) v
exact Z.coordChange_comp i j k x hx v