continuous_totalSpaceMk — Mathlib

English

TotalSpace.mk is continuous in the pullback setting, under suitable assumptions.

Русский

TotalSpace.mk непрерывно в ситуации pullback при подходящих предположениях.

LaTeX

$$$\mathrm{ContinuousTotalSpaceMk}$$$

Lean4

theorem continuous_totalSpaceMk [∀ x, TopologicalSpace (E x)] [FiberBundle F E] {f : B' → B} {x : B'} :
    Continuous (@TotalSpace.mk _ F (f *ᵖ E) x) :=
  by
  simp only [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, induced_compose, induced_inf,
    Function.comp_def, induced_const, top_inf_eq, pullbackTopology_def]
  exact (FiberBundle.totalSpaceMk_isInducing F E (f x)).eq_induced.le

Похожие утверждения