English
Each linear trivialization is in fact a continuous linear equivalence between the fiber and the model fiber, with linear inverse given by the backward map.
Русский
Каждая линейная тривиализация на деле образует непрерывное линейное эквивалентность между фиброй и модельной фиброй, с обратным линейным отображением, заданным обратным отображением.
LaTeX
$$$E_b \cong_L[R] F \quad (\text{for each } b)\,$$$
Lean4
/-- In a vector bundle, a trivialization in the fiber (which is a priori only linear)
is in fact a continuous linear equiv between the fibers and the model fiber. -/
@[simps -fullyApplied apply symm_apply]
def continuousLinearEquivAt (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) (hb : b ∈ e.baseSet) : E b ≃L[R] F :=
{
e.toPretrivialization.linearEquivAt R b
hb with
toFun := fun y =>
(e ⟨b, y⟩).2 -- given explicitly to help `simps`
invFun := e.symm b
continuous_toFun :=
(e.continuousOn.comp_continuous (FiberBundle.totalSpaceMk_isInducing F E b).continuous fun _ =>
e.mem_source.mpr hb).snd
continuous_invFun := (e.symmL R b).continuous }
