continuousInv_of_discreteTopology

English

If H has a discrete topology, then the inversion is continuous on H.

Русский

Если у группы H дискретная топология, то обратное отображение непрерывно на H.

LaTeX

$$$\\\\operatorname{ContinuousInv} H$ при дискретной топологии.$$

Lean4

@[to_additive]
instance (priority := 100) continuousInv_of_discreteTopology [TopologicalSpace H] [Inv H] [DiscreteTopology H] :
    ContinuousInv H :=
  ⟨continuous_of_discreteTopology⟩

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