isQuotientMap_proj — Mathlib

English

The projection is a quotient map (under nonempty fiber).

Русский

Проекция является факторным (квотизируемым) отображением при непустом волокне.

LaTeX

$$IsQuotientMap(\pi F E)$$

Lean4

/-- The projection from a fiber bundle with a nonempty fiber to its base is a quotient
map. -/
theorem isQuotientMap_proj [Nonempty F] : IsQuotientMap (π F E) :=
  (isOpenMap_proj F E).isQuotientMap (continuous_proj F E) (surjective_proj F E)

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