isClosedMap_prodMk_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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