English
The coordinate change induces a homeomorphism on the fiber: for any b ∈ baseSet, h1 and h2 in baseSet yield a homeomorphism F ≃ₜ F with toFun = e1.coordChange e2 b, invFun = e2.coordChange e1 b, and continuous maps.
Русский
Переход координат порождает гомоморфизм в виде гомоморфа по волокну; для любых b в базовом множестве существует гомеоморфизм F ≃ₜ F с функциями toFun и invFun, задаваемыми переходами координат.
LaTeX
$$\\text{coordChangeHomeomorph}(e_1,e_2,h_1,h_2) : F ≃ₜ F with toFun = e_1.coordChange e_2 b, invFun = e_2.coordChange e_1 b$$
Lean4
theorem continuous_coordChange (e₁ e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) :
Continuous (e₁.coordChange e₂ b) :=
by
refine
continuous_snd.comp
(e₂.toOpenPartialHomeomorph.continuousOn.comp_continuous
(e₁.toOpenPartialHomeomorph.continuousOn_symm.comp_continuous ?_ ?_) ?_)
· fun_prop
· exact fun x => e₁.mem_target.2 h₁
· intro x
rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]
