English
The target component of the trivialization is continuous in the base chart.
Русский
Компонента цели тривиализации непрерывна в базовой схеме.
LaTeX
$$$ (\\operatorname{trivializationAt} (F_1 \\to SL[\\sigma] F_2) (\\cdot) x_0).target = ((\\operatorname{trivializationAt} F_1 E_1 x_0).baseSet \\cap (\\operatorname{trivializationAt} F_2 E_2 x_0).baseSet) \\times \\text{univ} $$$
Lean4
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a basemap `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is `C^n`. -/
theorem clm_bundle_apply
(hϕ :
ContinuousWithinAt (fun m ↦ TotalSpace.mk' (F₁ →L[𝕜] F₂) (E := fun (x : B) ↦ (E₁ x →L[𝕜] E₂ x)) (b m) (ϕ m)) s x)
(hv : ContinuousWithinAt (fun m ↦ TotalSpace.mk' F₁ (b m) (v m)) s x) :
ContinuousWithinAt (fun m ↦ TotalSpace.mk' F₂ (b m) (ϕ m (v m))) s x :=
by
simp only [continuousWithinAt_hom_bundle] at hϕ
exact hϕ.2.clm_apply_of_inCoordinates hv hϕ.1
