t4Space

Mathlib.Topology.EMetricSpace.Paracompact

URI: https://scilib.ai/kg/mathlib#EMetric.t4Space

English

Any EMetricSpace is a T4 space (normal Hausdorff).

Русский

Любое EMetricSpace является T4-пространством (нормальное и Hausdorff).

LaTeX

$$$T4Space(\\alpha)$$$

Lean4

theorem t4Space [EMetricSpace α] : T4Space α :=
  inferInstance

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

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

Разделы

Аффилиация

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