continuous_totalSpaceMk — Mathlib

English

The map assigning to b the total-space point mk b is continuous with respect to the total-space topology on TotalSpace F E.

Русский

Отображение b ↦ mk(b) непрерывно относительно топологии полного пространства TotalSpace F E.

LaTeX

$$$$ \\text{continuous_totalSpaceMk}(a)(b) : \\text{Continuous} \\; (\\\\mathrm{TotalSpace.mk} \\, b) $$$$

Lean4

@[continuity]
theorem continuous_totalSpaceMk (b : B) : Continuous[_, a.totalSpaceTopology] (.mk b) :=
  a.toFiberPrebundle.continuous_totalSpaceMk b

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