t1Space — Mathlib

English

If the identity element {1} is a closed subset in a topological group G, then G is a T1 space.

Русский

Если множество {1} замкнуто в топологической группе G, то G является пространством T1.

LaTeX

$$$\\operatorname{IsClosed}(\\{1\\}) \\Rightarrow T_1\\text{-space}(G)$$$

Lean4

@[to_additive]
theorem t1Space (h : @IsClosed G _ { 1 }) : T1Space G :=
  ⟨fun x => by simpa using isClosedMap_mul_right x _ h⟩

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