isOpenMap_mkQ

Mathlib.Topology.Algebra.Module.Basic

URI: https://scilib.ai/kg/mathlib#Submodule.isOpenMap_mkQ

English

The quotient map S.mkQ is open when M has a topological group structure and the module operations are continuous.

Русский

Квартиантная карта S.mkQ является открытой, если M имеет топологическую группу и операции модуля непрерывны.

LaTeX

$$$\text{IsOpenMap}(S.mkQ)$$$

Lean4

theorem isOpenMap_mkQ [ContinuousAdd M] : IsOpenMap S.mkQ :=
  QuotientAddGroup.isOpenMap_coe

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

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

Разделы

Аффилиация

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