English
The composition of two local trivializations corresponds to a trivialization change: the i-to-j composition equals the trivialization change Z.trivChange i j.
Русский
Сложение двух локальных тривиализаций соответствует изменению тривиализации: композиция i→j равна Z.trivChange i j.
LaTeX
$$$ (Z.localTrivAsPartialEquiv i)^{\\!-1} \\; \\cdot\\; Z.localTrivAsPartialEquiv j \\; \\approx\\; (Z.trivChange i j).\\text{toPartialEquiv}$$$
Lean4
/-- The composition of two local trivializations is the trivialization change Z.triv_change i j. -/
theorem localTrivAsPartialEquiv_trans (i j : ι) :
(Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j) ≈ (Z.trivChange i j).toPartialEquiv :=
by
constructor
· ext x
simp only [mem_localTrivAsPartialEquiv_target, mfld_simps]
rfl
· rintro ⟨x, v⟩ hx
simp only [trivChange, localTrivAsPartialEquiv, PartialEquiv.symm, Prod.mk_inj, prodMk_mem_set_prod_eq,
PartialEquiv.trans_source, mem_inter_iff, mem_preimage, proj, mem_univ, (· ∘ ·), PartialEquiv.coe_trans] at hx ⊢
simp only [Z.coordChange_comp, hx, mem_inter_iff, and_self_iff, mem_baseSet_at]
