instT2Space

Mathlib.Topology.Algebra.Constructions.DomMulAct

URI: https://scilib.ai/kg/mathlib#DomMulAct.instT2Space

English

If M is T2 (Hausdorff), then Mᵈᵐᵃ is T2.

Русский

Если M является пространством T2 (Гаусдорфово), то Mᵈᵐᵃ также T2.

LaTeX

$$$ [T2Space\\ M] \\, \\Rightarrow \\, T2Space\\ M^{\\mathrm{DM}}$$

Lean4

@[to_additive]
instance instT2Space [T2Space M] : T2Space Mᵈᵐᵃ :=
  mkHomeomorph.t2Space

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru