surjective_mk

Mathlib.Topology.Separation.Hausdorff

URI: https://scilib.ai/kg/mathlib#T2Quotient.surjective_mk

English

The quotient map mk is continuous.

Русский

Отображение mk непрерывно.

LaTeX

$$$ Continuous(mk:X\\to T2Quotient X)$$$

Lean4

theorem surjective_mk : Surjective (mk : X → T2Quotient X) :=
  Quotient.mk_surjective

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

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

Разделы

Аффилиация

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