isClosedMap_mk

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.isClosedMap_mk

English

The quotient map mk is a closed map.

Русский

Квазиотображение mk является замкнутым отображением.

LaTeX

$$$\\text{IsClosedMap}(\\mathrm{mk})$$$

Lean4

theorem isClosedMap_mk : IsClosedMap (mk : X → SeparationQuotient X) :=
  isInducing_mk.isClosedMap <| by rw [range_mk]; exact isClosed_univ

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru