instIsTopologicalGroup — Mathlib

English

There is a natural topological group structure on ContinuousMonoidHom A E provided A,E with the appropriate topologies and group structures.

Русский

Существует естественная структура топологической группы на ContinuousMonoidHom A E при заданных топологиях и групповых структурах.

LaTeX

$$$\text{IsTopologicalGroup}(\mathrm{ContinuousMonoidHom}\, A\, E).$$$

Lean4

@[to_additive]
instance : IsTopologicalGroup (ContinuousMonoidHom A E) :=
  let hi := isInducing_toContinuousMap A E
  let hc := hi.continuous
  { continuous_mul := hi.continuous_iff.mpr (continuous_mul.comp (Continuous.prodMap hc hc))
    continuous_inv := hi.continuous_iff.mpr (continuous_inv.comp hc) }

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