English
Two coordinate-change homeomorphs corresponding to equal trivializations are equal; i.e., congruence implies equality of the homeomorphs.
Русский
Две гомеоморфные карты перехода координат совпадают при равенстве тривиализаций.
LaTeX
$$$e_1.coordChangeHomeomorph e_2 h_1 h_2 = e'_1.coordChangeHomeomorph e'_2 h'_1 h'_2$ whenever the corresponding equalities hold$$
Lean4
/-- Coordinate transformation in the fiber induced by a pair of bundle trivializations,
as a homeomorphism. -/
protected def coordChangeHomeomorph (e₁ e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet)
(h₂ : b ∈ e₂.baseSet) : F ≃ₜ F where
toFun := e₁.coordChange e₂ b
invFun := e₂.coordChange e₁ b
left_inv x := by simp only [*, coordChange_coordChange, coordChange_same_apply]
right_inv x := by simp only [*, coordChange_coordChange, coordChange_same_apply]
continuous_toFun := e₁.continuous_coordChange e₂ h₁ h₂
continuous_invFun := e₂.continuous_coordChange e₁ h₂ h₁
