instT2Space

Mathlib.Topology.Algebra.Constructions

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

English

If M is a Hausdorff space, then Mᵐᵒᵖ is Hausdorff.

Русский

Если пространство M Гаусдорфово, то Mᵐᵒᵖ тоже Гаусдорфово.

LaTeX

$$$$ \operatorname{T2Space}(M) \Rightarrow \operatorname{T2Space}(M^{\mathrm{op}}) $$$$

Lean4

@[to_additive]
instance instT2Space [T2Space M] : T2Space Mᵐᵒᵖ :=
  opHomeomorph.t2Space

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

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

Разделы

Аффилиация

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