English
Natural identification of VectorPrebundle as FiberPrebundle: the prebundle data provides a FiberPrebundle with the same total-space topology and projection.
Русский
Естественная идентификация VectorPrebundle как FiberPrebundle: данные предтривиализации задают FiberPrebundle с той же топологией полного пространства и проекцией.
LaTeX
$$$$ toFiberPrebundle(a) : FiberPrebundle F E $$$$
Lean4
/-- Make a `VectorBundle` from a `VectorPrebundle`. Concretely this means
that, given a `VectorPrebundle` structure for a sigma-type `E` -- which consists of a
number of "pretrivializations" identifying parts of `E` with product spaces `U × F` -- one
establishes that for the topology constructed on the sigma-type using
`VectorPrebundle.totalSpaceTopology`, these "pretrivializations" are actually
"trivializations" (i.e., homeomorphisms with respect to the constructed topology). -/
theorem toVectorBundle : @VectorBundle R _ F E _ _ _ _ _ _ a.totalSpaceTopology _ a.toFiberBundle :=
letI := a.totalSpaceTopology;
letI := a.toFiberBundle
{ trivialization_linear' := by
rintro _ ⟨e, he, rfl⟩
apply linear_trivializationOfMemPretrivializationAtlas
continuousOn_coordChange' := by
rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩
refine (a.continuousOn_coordChange he he').congr fun b hb ↦ ?_
ext v
haveI h₁ := a.linear_trivializationOfMemPretrivializationAtlas he
haveI h₂ := a.linear_trivializationOfMemPretrivializationAtlas he'
rw [trivializationOfMemPretrivializationAtlas] at h₁ h₂
rw [a.coordChange_apply he he' hb v, ContinuousLinearEquiv.coe_coe, Trivialization.coordChangeL_apply]
exacts [rfl, hb] }
