English
In a Hausdorff topological group, any subgroup with the discrete topology is a closed subset.
Русский
В гиперболической топологической группе любая подгруппа с дискретной топологией является замкнутым подмножеством.
LaTeX
$$$[T2Space\ G] \,{H : Subgroup\ G}\[DiscreteTopology\ H] : IsClosed (H : Set\ G).$$$
Lean4
@[to_additive]
instance isClosed_of_discrete [T2Space G] {H : Subgroup G} [DiscreteTopology H] : IsClosed (H : Set G) :=
by
obtain ⟨V, V_in, VH⟩ : ∃ (V : Set G), V ∈ 𝓝 (1 : G) ∧ V ∩ (H : Set G) = { 1 } :=
nhds_inter_eq_singleton_of_mem_discrete H.one_mem
have : (fun p : G × G => p.2 / p.1) ⁻¹' V ∈ 𝓤 G := preimage_mem_comap V_in
apply isClosed_of_spaced_out this
intro h h_in h' h'_in
contrapose!
simp only [Set.mem_preimage]
rintro (hyp : h' / h ∈ V)
have : h' / h ∈ ({ 1 } : Set G) := VH ▸ Set.mem_inter hyp (H.div_mem h'_in h_in)
exact (eq_of_div_eq_one this).symm
