continuous_totalSpaceMk — Mathlib

English

For each base point x in B, the map from the fiber E_x into the total space given by TotalSpace.mk x is continuous.

Русский

Для каждой базовой точки x ∈ B отображение из волокна E_x в общее пространство, задаваемое TotalSpace.mk x, непрерывно.

LaTeX

$$$\forall x\in B,\ \operatorname{Continuous}(\operatorname{TotalSpace.mk}\ x)$$$

Lean4

theorem continuous_totalSpaceMk (x : B) : Continuous (@TotalSpace.mk B F E x) :=
  (totalSpaceMk_isInducing F E x).continuous

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