isOpenMap_proj — Mathlib

English

The projection map proj: Z → B is an open map: it sends open sets to open sets in B.

Русский

Пусть проекция proj: Z → B является открытым отображением: образ открытых множеств подproj открыт в B.

LaTeX

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

Lean4

/-- The projection from a trivial fiber bundle to its base is open. -/
protected theorem isOpenMap_proj (h : IsHomeomorphicTrivialFiberBundle F proj) : IsOpenMap proj := by
  obtain ⟨e, rfl⟩ := h.proj_eq; exact isOpenMap_fst.comp e.isOpenMap

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