English
If e1 and e2 are trivializations, then the fiber coordinate change map b ↦ e1.coordChange e2 b is a continuous function on the base set, with the appropriate domain restrictions.
Русский
Переход координат по волокну непрерывен на базовом множестве при двух тривиализациях.
LaTeX
$$$\\text{Continuous}(e_1.coordChange e_2)$$
Lean4
/-- Restrict a `Trivialization` to an open set in the base. -/
protected def restrOpen (e : Trivialization F proj) (s : Set B) (hs : IsOpen s) : Trivialization F proj
where
toOpenPartialHomeomorph :=
((e.isImage_preimage_prod s).symm.restr (IsOpen.inter e.open_target (hs.prod isOpen_univ))).symm
baseSet := e.baseSet ∩ s
open_baseSet := IsOpen.inter e.open_baseSet hs
source_eq := by simp [source_eq]
target_eq := by simp [target_eq, prod_univ]
proj_toFun p hp := e.proj_toFun p hp.1
