isClosedMap_prodMk_right — Mathlib

English

The map x ↦ (x,y) is a closed map for fixed y in a product X × Y.

Русский

Отображение x ↦ (x,y) нафиксированное y является замкнутое отображение на произведении X × Y.

LaTeX

$$$ \text{IsClosedMap}(\lambda x:X, (x,y))$.$$

Lean4

theorem isClosedMap_prodMk_right [TopologicalSpace Y] [T1Space Y] (y : Y) : IsClosedMap (fun x : X ↦ Prod.mk x y) :=
  fun _K hK ↦ Set.prod_singleton ▸ hK.prod isClosed_singleton

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