English
From a pretrivialization e in the atlas, one obtains a corresponding trivialization on the same total space compatible with the total space topology.
Русский
Из предтривиализации e в атласе получается соответствующая тривиализация над тем же полным пространством, совместимая сTopology полного пространства.
LaTeX
$$$ \exists t: \text{Trivialization}(F, \pi F E),\ t = a.trivializationOfMemPretrivializationAtlas(e) \text{ for } e \in a.pretrivializationAtlas $$$
Lean4
/-- Promotion from a `Pretrivialization` to a `Trivialization`. -/
def trivializationOfMemPretrivializationAtlas (he : e ∈ a.pretrivializationAtlas) :
@Trivialization B F _ _ _ a.totalSpaceTopology (π F E) :=
let _ := a.totalSpaceTopology
{ e with
open_source := a.isOpen_source e,
continuousOn_toFun :=
by
refine
continuousOn_iff'.mpr fun s hs =>
⟨e ⁻¹' s ∩ e.source, isOpen_iSup_iff.mpr fun e' => ?_, by rw [inter_assoc, inter_self]; rfl⟩
refine isOpen_iSup_iff.mpr fun he' => ?_
rw [isOpen_coinduced, isOpen_induced_iff]
obtain ⟨u, hu1, hu2⟩ := continuousOn_iff'.mp (a.continuous_trivChange _ he _ he') s hs
have hu3 := congr_arg (fun s => (fun x : e'.target => (x : B × F)) ⁻¹' s) hu2
simp only [Subtype.coe_preimage_self, preimage_inter, univ_inter] at hu3
refine
⟨u ∩ e'.toPartialEquiv.target ∩ e'.toPartialEquiv.symm ⁻¹' e.source, ?_, by
simp only [preimage_inter, inter_univ, Subtype.coe_preimage_self, hu3.symm]; rfl⟩
rw [inter_assoc]
exact hu1.inter (a.isOpen_target_of_mem_pretrivializationAtlas_inter e e' he')
continuousOn_invFun := a.continuous_symm_of_mem_pretrivializationAtlas he }
