linear_trivializationOfMemPretrivializationAtlas

English

There is a linear trivialization associated to a pretrivialization in a VectorPrebundle, making the corresponding trivialization linear over the base field.

Русский

Существует линейная тривиализация, связанная с предтривиализацией в VectorPrebundle, делающая тривиализацию линейной над базовым полем.

LaTeX

$$$$ \\text{Trivialization.IsLinear}(R, \\text{trivializationOfMemPretrivializationAtlas}(a,he)) $$$$

Lean4

theorem linear_trivializationOfMemPretrivializationAtlas (a : VectorPrebundle R F E) {e : Pretrivialization F (π F E)}
    (he : e ∈ a.pretrivializationAtlas) :
    letI := a.totalSpaceTopology
    Trivialization.IsLinear R (trivializationOfMemPretrivializationAtlas a he) :=
  letI := a.totalSpaceTopology
  { linear := (a.pretrivialization_linear' e he).linear }

Похожие утверждения