isOpenMap_mk

Mathlib.Topology.Inseparable

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

← MathLib Explorer

English

The quotient map mk is an open map.

Русский

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

LaTeX

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

Lean4

theorem isOpenMap_mk : IsOpenMap (mk : X → SeparationQuotient X) := fun s hs =>
  isQuotientMap_mk.isOpen_preimage.1 <| by rwa [preimage_image_mk_open hs]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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