t3_quotient_of_isClosed — Mathlib

English

If M is a topological additive group and S is a closed submodule, then the quotient M/S is a T3-space.

Русский

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

LaTeX

$$$T3Space(M/S).$$$

Lean4

instance t3_quotient_of_isClosed [IsTopologicalAddGroup M] [IsClosed (S : Set M)] : T3Space (M ⧸ S) :=
  letI : IsClosed (S.toAddSubgroup : Set M) := ‹_›
  QuotientAddGroup.instT3Space S.toAddSubgroup

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