instT2Space

Mathlib.Analysis.Complex.Basic

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

English

The complex plane ℂ is a Hausdorff space.

Русский

Плоскость комплексных чисел ℂ является хаусдорфовым пространством.

LaTeX

$$$$ \\text{Hausdorff}(\\mathbb{C}). $$$$

Lean4

instance instT2Space : T2Space ℂ :=
  TopologicalSpace.t2Space_of_metrizableSpace

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

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

Разделы

Аффилиация

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