isOpenMap_fst — Mathlib

English

The first projection in a product of topological spaces is an open map.

Русский

Первая проекция в произведении топологических пространств является открытым отображением.

LaTeX

$$$$IsOpenMap(\mathrm{Prod.fst})$$$$

Lean4

/-- The first projection in a product of topological spaces sends open sets to open sets. -/
theorem isOpenMap_fst : IsOpenMap (@Prod.fst X Y) :=
  isOpenMap_iff_nhds_le.2 fun x => (map_fst_nhds x).ge

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