topologicalAddGroup_quotient — Mathlib

English

If M is a topological additive group and S a submodule, the quotient M/S inherits a natural topology making it a topological additive group.

Русский

Пусть M — топологическая аддитивная группа, и S — подмодуль. Тогда фактор-множество M/S получает естественную топологию и является топологической аддитивной группой.

LaTeX

$$$M/S\\text{ is a topological additive group.}$$$

Lean4

instance topologicalAddGroup_quotient [IsTopologicalAddGroup M] : IsTopologicalAddGroup (M ⧸ S) :=
  inferInstanceAs <| IsTopologicalAddGroup (M ⧸ S.toAddSubgroup)

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