English
A fiber bundle core determines a genuine fiber bundle with base B and fiber F; its total space is Z.TotalSpace and its fiber is Z.Fiber.
Русский
Ядро фибер-расслоения задаёт настоящие фибер-расслоение с основанием B и волокном F; общая часть пространства — Z.TotalSpace, а волокно — Z.Fiber.
LaTeX
$$$ (Z.TotalSpace, Z.proj) \text{ is a fiber bundle over } B \text{ with fiber } Z.Fiber. $$$
Lean4
/-- A fiber bundle constructed from core is indeed a fiber bundle. -/
instance fiberBundle : FiberBundle F Z.Fiber
where
totalSpaceMk_isInducing'
b :=
isInducing_iff_nhds.2 fun x ↦
by
rw [(Z.localTrivAt b).nhds_eq_comap_inf_principal (mk_mem_localTrivAt_source _ _ _), comap_inf, comap_principal,
comap_comap]
simp only [Function.comp_def, localTrivAt_apply_mk, Trivialization.coe_coe,
← (isEmbedding_prodMkRight b).nhds_eq_comap]
convert_to 𝓝 x = 𝓝 x ⊓ 𝓟 univ
· congr
exact eq_univ_of_forall (mk_mem_localTrivAt_source Z _)
· rw [principal_univ, inf_top_eq]
trivializationAtlas' := Set.range Z.localTriv
trivializationAt' := Z.localTrivAt
mem_baseSet_trivializationAt' := Z.mem_baseSet_at
trivialization_mem_atlas' b := ⟨Z.indexAt b, rfl⟩
