isOpenMap_snd — Mathlib

English

The first projection is a quotient map when Y is nonempty.

Русский

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

LaTeX

$$$$IsQuotientMap(\mathrm{Prod.fst}):\text{ при }\mathsf{Nonempty}(Y).$$$$

Lean4

/-- The second projection in a product of topological spaces sends open sets to open sets. -/
theorem isOpenMap_snd : IsOpenMap (@Prod.snd X Y) :=
  isOpenMap_iff_nhds_le.2 fun x => (map_snd_nhds x).ge

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