English
If e is a trivialization with fiber F and h is a homeomorphism F ≃ₜ F', then e.transFiberHomeomorph h is the trivialization with fiber F' given by sending z ∈ Z to ((e z).1, h((e z).2)).
Русский
Если e — тривиализация с волокном F и h — гомеморфизм F ≃ₜ F', то e.transFiberHomeomorph h — тривиализация с волокном F', отправляющая z ∈ Z в ((e z).1, h((e z).2)).
LaTeX
$$$\\text{transFiberHomeomorph}(e,h) \\\\\$$
Lean4
/-- If `e` is a `Trivialization` of `proj : Z → B` with fiber `F` and `h` is a homeomorphism
`F ≃ₜ F'`, then `e.trans_fiber_homeomorph h` is the trivialization of `proj` with the fiber `F'`
that sends `p : Z` to `((e p).1, h (e p).2)`. -/
def transFiberHomeomorph {F' : Type*} [TopologicalSpace F'] (e : Trivialization F proj) (h : F ≃ₜ F') :
Trivialization F' proj
where
toOpenPartialHomeomorph := e.toOpenPartialHomeomorph.transHomeomorph <| (Homeomorph.refl _).prodCongr h
baseSet := e.baseSet
open_baseSet := e.open_baseSet
source_eq := e.source_eq
target_eq := by simp [target_eq, prod_univ, preimage_preimage]
proj_toFun := e.proj_toFun
