instT2Space — Mathlib

English

If M is a T2 (Hausdorff) space, then the unit group Mˣ, with the subspace topology, is also a T2 space.

Русский

Если M — пространство типа T2 (хаусдорфово), то группа единиц Mˣ с подподстановкой той же топологии также является пространством T2.

LaTeX

$$$\\forall M\\, [T2Space\\, M]\\Rightarrow T2Space\\, M^\\times$$$

Lean4

@[to_additive]
instance instT2Space [T2Space M] : T2Space Mˣ :=
  isEmbedding_embedProduct.t2Space

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