continuous_mk

Mathlib.Topology.Algebra.Group.Quotient

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

English

The quotient map mk: G → G/N is continuous.

Русский

Карта перехода mk: G → G/N непрерывна.

LaTeX

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

Lean4

@[to_additive (attr := continuity, fun_prop)]
theorem continuous_mk {N : Subgroup G} : Continuous (mk : G → G ⧸ N) :=
  continuous_quot_mk

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

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

Разделы

Аффилиация

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