mem_trivialization_at_source — Mathlib

English

From a VectorPrebundle, one obtains a VectorBundle structure on the total space, i.e., the prebundle data along with the total-space topology yields a genuine vector bundle.

Русский

Из VectorPrebundle получается структура VectorBundle на полном пространстве: предтривиализация вместе с топологией полного пространства образует вещественное векторное волокно.

LaTeX

$$$$ \\text{toVectorBundle}(a) : \\text{VectorBundle} \\; R\\; F\\; E $$$$

Lean4

theorem mem_trivialization_at_source (b : B) (x : E b) : ⟨b, x⟩ ∈ (a.pretrivializationAt b).source :=
  a.toFiberPrebundle.mem_pretrivializationAt_source b x

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