isClosedMap_const — Mathlib

English

A constant map from X to Y into a T1-space Y is a closed map.

Русский

Постоянное отображение из X в Y в T1-пространстве Y является замкнутым отображением.

LaTeX

$$$ \text{IsClosedMap}(\mathrm{const}_{X}\, y)$ for any y ∈ Y.$$

Lean4

theorem isClosedMap_const {X Y} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {y : Y} :
    IsClosedMap (Function.const X y) :=
  IsClosedMap.of_nonempty fun s _ h2s => by simp_rw [const, h2s.image_const, isClosed_singleton]

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