isQuotientMap_proj — Mathlib

English

The projection map proj: Z → B is a quotient map.

Русский

Проекция proj: Z → B является квазиобразующей картой (quotient map).

LaTeX

$$$\mathrm{IsQuotientMap}(\mathrm{proj})$$$

Lean4

/-- The projection from a trivial fiber bundle to its base is open. -/
protected theorem isQuotientMap_proj [Nonempty F] (h : IsHomeomorphicTrivialFiberBundle F proj) : IsQuotientMap proj :=
  h.isOpenMap_proj.isQuotientMap h.continuous_proj h.surjective_proj

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