English
In a vector bundle with a linear trivialization, the forward map at each base point b is a continuous linear map from the fiber E_b to the model fiber F, defined for every b.
Русский
Векторное расслоение с линейной тривиализацией: отображение вперёд на каждой точке базы $b$ есть непрерывное линейное отображение из фибры $E_b$ в модельную фибру $F$, и оно определено для всех $b$.
LaTeX
$$$\forall b,\ e.continuousLinearMapAt(R, b): E_b \to_L[R] F,$$$
Lean4
/-- Forward map of `Trivialization.continuousLinearEquivAt` (only propositionally equal),
defined everywhere (`0` outside domain). -/
@[simps -fullyApplied apply]
def continuousLinearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) : E b →L[R] F :=
{ e.linearMapAt R b with
toFun := e.linearMapAt R b
cont := by
rw [e.coe_linearMapAt b]
classical
refine continuous_if_const _ (fun hb => ?_) fun _ => continuous_zero
exact
(e.continuousOn.comp_continuous (FiberBundle.totalSpaceMk_isInducing F E b).continuous fun x =>
e.mem_source.mpr hb).snd }
