isOpenQuotientMap_mk

Mathlib.Topology.Inseparable

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

English

mk is an open quotient map, i.e., surjective, continuous, and open.

Русский

mk — открытое квота-отображение, то есть сюръективно, непрерывно и открыто.

LaTeX

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

Lean4

theorem isOpenQuotientMap_mk : IsOpenQuotientMap (mk : X → SeparationQuotient X) :=
  ⟨surjective_mk, continuous_mk, isOpenMap_mk⟩

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

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

Разделы

Аффилиация

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