instT3Space — Mathlib

English

If N is normal and closed, then the quotient has T3 separation property.

Русский

Если N нормальна и замкнута, то фактор-группа обладает свойством разделимости T3.

LaTeX

$$$[N.Normal] \land [IsClosed(N)] \Rightarrow T3Space (G ⧸ N).$$$

Lean4

@[to_additive]
instance instT3Space [N.Normal] [hN : IsClosed (N : Set G)] : T3Space (G ⧸ N) :=
  by
  rw [← QuotientGroup.ker_mk' N] at hN
  haveI := IsTopologicalGroup.t1Space (G ⧸ N) ((isQuotientMap_mk N).isClosed_preimage.mp hN)
  infer_instance

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