isOpenMap_proj — Mathlib

English

The projection on the base is an open map: images of open sets in the total space are open in the base.

Русский

Проекция на основание — открытое отображение: изображения открытых множеств в полном пространстве являются открытыми на основании.

LaTeX

$$$ IsOpenMap\ Z.proj $$$

Lean4

/-- The projection on the base of a fiber bundle created from core is an open map -/
nonrec theorem isOpenMap_proj : IsOpenMap Z.proj :=
  FiberBundle.isOpenMap_proj F Z.Fiber

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