topologicalGroup_of_discreteTopology

English

Any group with a discrete topology is a topological group.

Русский

Любая группа с дискретной топологией является топологической группой.

LaTeX

$$$[TopologicalSpace H] \\land [Group H] \\land [DiscreteTopology H] \\Rightarrow IsTopologicalGroup H.$$$

Lean4

@[to_additive]
instance (priority := 100) topologicalGroup_of_discreteTopology [TopologicalSpace H] [Group H] [DiscreteTopology H] :
    IsTopologicalGroup H :=
  ⟨⟩

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