continuous_proj — Mathlib

English

The projection map from the total space to the base is continuous for the fiber bundle constructed from a core.

Русский

Проекция из полного пространства на основание непрерывна для фибер-бандла, построенного из ядра.

LaTeX

$$$ \text{Continuous} \ Z.proj $$$

Lean4

/-- The projection on the base of a fiber bundle created from core is continuous -/
nonrec theorem continuous_proj : Continuous Z.proj :=
  FiberBundle.continuous_proj F Z.Fiber

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