English
From a FiberPrebundle a, one constructs a FiberBundle structure on the total space with atlas drawn from trivializations corresponding to pretrivializations.
Русский
Из FiberPrebundle a строится структура FiberBundle на полном пространстве с атласом, соответствующим тривиализациям, связанным с предтривиализациями.
LaTeX
$$$ toFiberBundle(a) : FiberBundle F E $$$
Lean4
/-- Make a `FiberBundle` from a `FiberPrebundle`. Concretely this means
that, given a `FiberPrebundle` 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
`FiberPrebundle.totalSpaceTopology`, these "pretrivializations" are actually
"trivializations" (i.e., homeomorphisms with respect to the constructed topology). -/
def toFiberBundle : @FiberBundle B F _ _ E a.totalSpaceTopology _ :=
let _ := a.totalSpaceTopology
{ totalSpaceMk_isInducing' := fun b ↦ a.inducing_totalSpaceMk_of_inducing_comp b (a.totalSpaceMk_isInducing b)
trivializationAtlas' :=
{e | ∃ (e₀ : _) (he₀ : e₀ ∈ a.pretrivializationAtlas), e = a.trivializationOfMemPretrivializationAtlas he₀},
trivializationAt' := fun x ↦ a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas x),
mem_baseSet_trivializationAt' := a.mem_base_pretrivializationAt
trivialization_mem_atlas' := fun x ↦ ⟨_, a.pretrivialization_mem_atlas x, rfl⟩ }
