isOpenMap_coe

Mathlib.Topology.Algebra.Group.Quotient

URI: https://scilib.ai/kg/mathlib#QuotientGroup.isOpenMap_coe

English

The quotient map mk is an open quotient map.

Русский

Карта перехода mk является открытой факторной картой.

LaTeX

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

Lean4

@[to_additive]
theorem isOpenMap_coe : IsOpenMap ((↑) : G → G ⧸ N) :=
  isOpenMap_quotient_mk'_mul

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

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

Разделы

Аффилиация

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