isOpenQuotientMap_mkQ — Mathlib

English

Let M be a topological module and S a submodule. Then the canonical projection π: M → M/S is an open quotient map.

Русский

Пусть M — топологический модуль, S — подмодуль. Тогда каноническое проецирование π: M → M/S является открытым отображением на факторпространстве.

LaTeX

$$$\\\\pi: M \\\\to M/S \\\\quad\\\\text{is an open map, i.e. } \\\\forall U \\\\in \\\\mathcal{T}(M), \\\\pi[U] \\\\in \\\\mathcal{T}(M/S).$$$

Lean4

theorem isOpenQuotientMap_mkQ [ContinuousAdd M] : IsOpenQuotientMap S.mkQ :=
  QuotientAddGroup.isOpenQuotientMap_mk

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