t2Space_iff_one_closed

Mathlib.Topology.Algebra.Group.Pointwise

URI: https://scilib.ai/kg/mathlib#IsTopologicalGroup.t2Space_iff_one_closed

← MathLib Explorer

English

Every topological group is a regular space.

Русский

Каждая топологическая группа является регулярным пространством.

LaTeX

$$$\\text{RegularSpace}(G)\\quad\\text{for a topological group } G$$$

Lean4

@[to_additive]
theorem t2Space_iff_one_closed : T2Space G ↔ IsClosed ({ 1 } : Set G) :=
  ⟨fun _ ↦ isClosed_singleton, fun h ↦
    have := IsTopologicalGroup.t1Space G h;
    inferInstance⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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