English
For a vector bundle core, the coordinate change maps satisfy associativity: coordChange j k x after coordChange i j x equals coordChange i k x, on overlapping base sets.
Русский
Для ядра векторного расслоения переходы координат удовлетворяют ассоциативности на пересечении базовых множеств.
LaTeX
$$$(\coordChange j k x) \circ (\coordChange i j x) = \coordChange i k x$ for x in the triple intersection of base sets$$
Lean4
theorem symm_apply_eq_mk_continuousLinearEquivAt_symm (e : Trivialization F (π F E)) [e.IsLinear R] (b : B)
(hb : b ∈ e.baseSet) (z : F) :
e.toOpenPartialHomeomorph.symm ⟨b, z⟩ = ⟨b, (e.continuousLinearEquivAt R b hb).symm z⟩ :=
by
have h : (b, z) ∈ e.target := by
rw [e.target_eq]
exact ⟨hb, mem_univ _⟩
apply e.injOn (e.map_target h)
· simpa only [e.source_eq, mem_preimage]
·
simp_rw [e.right_inv h, coe_coe, e.apply_eq_prod_continuousLinearEquivAt R b hb,
ContinuousLinearEquiv.apply_symm_apply]
