English
If the composition a.pretrivializationAt(b) ∘ TotalSpace.mk b is inducing, then TotalSpace.mk b is inducing for the total space topology.
Русский
Если композиция a.pretrivializationAt(b) ∘ TotalSpace.mk b индуктивна, то TotalSpace.mk b индуктивна дляTopology полного пространства.
LaTeX
$$$ IsInducing\ (a.pretrivializationAt b \circ TotalSpace.mk b) \Rightarrow IsInducing (TotalSpace.mk b) $$$
Lean4
theorem inducing_totalSpaceMk_of_inducing_comp (b : B) (h : IsInducing (a.pretrivializationAt b ∘ TotalSpace.mk b)) :
@IsInducing _ _ _ a.totalSpaceTopology (TotalSpace.mk b) :=
by
letI := a.totalSpaceTopology
rw [← restrict_comp_codRestrict (a.mem_pretrivializationAt_source b)] at h
apply IsInducing.of_codRestrict (a.mem_pretrivializationAt_source b)
refine
h.of_comp ?_
(continuousOn_iff_continuous_restrict.mp
(a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas b)).continuousOn)
exact (a.continuous_totalSpaceMk b).codRestrict (a.mem_pretrivializationAt_source b)
