English
In a topological group, the space is T2 iff the singleton {1} is closed.
Русский
В топологической группе пространство является T2 тогда и только тогда, когда единичное множество {1} замкнуто.
LaTeX
$$$\\mathrm{T2Space}(G) \\iff \\mathrm{IsClosed}(\\{1\\})$$$
Lean4
@[to_additive]
instance (priority := 100) regularSpace : RegularSpace G :=
by
refine .of_exists_mem_nhds_isClosed_subset fun a s hs ↦ ?_
have : Tendsto (fun p : G × G => p.1 * p.2) (𝓝 (a, 1)) (𝓝 a) := continuous_mul.tendsto' _ _ (mul_one a)
rcases mem_nhds_prod_iff.mp (this hs) with ⟨U, hU, V, hV, hUV⟩
rw [← image_subset_iff, image_prod] at hUV
refine ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, ?_⟩
calc
closure U ⊆ closure U * interior V := subset_mul_left _ (mem_interior_iff_mem_nhds.2 hV)
_ = U * interior V := (isOpen_interior.closure_mul U)
_ ⊆ U * V := (mul_subset_mul_left interior_subset)
_ ⊆ s := hUV
