English
For a trivialization with a linear structure, the backward map from the model fiber F to the fiber E_b is also linear (fiberwise).
Русский
Для тривиализации с линейной структурой и обратное отображение от модели фибры к фибре над точкой базиса also линейно по каждой точке.
LaTeX
$$$\forall b,\ e.symmL(R, b): F \to_L[R] E_b$ является линейным отображением$$
Lean4
/-- Backwards map of `Trivialization.continuousLinearEquivAt`, defined everywhere. -/
@[simps -fullyApplied apply]
def symmL (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) : F →L[R] E b :=
{ e.symmₗ R b with
toFun := e.symm b
cont := by
by_cases hb : b ∈ e.baseSet
· rw [(FiberBundle.totalSpaceMk_isInducing F E b).continuous_iff]
exact e.continuousOn_symm.comp_continuous (.prodMk_right _) fun x ↦ mk_mem_prod hb (mem_univ x)
· refine continuous_zero.congr fun x => (e.symm_apply_of_notMem hb x).symm }
