English
Let R be a nontrivially normed field and E a vector bundle over B with typical fiber F. If e is a trivialization in the atlas of the bundle, then the fiberwise map e induces is a linear map E_b → F for every b in the base set of e.
Русский
Пусть R — ненулево нормированное поле, и имеется векторное расслоение E над B с типовым волокном F. Если e является тривиализацией, принадлежащей атласу расслоения, то на каждом основанном b отображение из фибра E_b в F линейно.
LaTeX
$$$\forall b \in e.baseSet,\ e.linearMapAt(R, b): E_b \to F\text{ является линейным отображением}$$$
Lean4
instance (priority := 100) trivialization_linear [VectorBundle R F E] (e : Trivialization F (π F E))
[MemTrivializationAtlas e] : e.IsLinear R :=
VectorBundle.trivialization_linear' e
