instIsTopologicalGroup — Mathlib

English

The quotient G/N is a topological group; the quotient inherits a group structure with continuous multiplication and inversion.

Русский

Фактор-группа G/N является топологической группой; структура группы и непрерывность умножения и обращения на неё наследуются от G.

LaTeX

$$$\text{IsTopologicalGroup}(G/N).$$$

Lean4

@[to_additive]
instance instIsTopologicalGroup [N.Normal] : IsTopologicalGroup (G ⧸ N)
    where
  continuous_mul := by
    rw [← (isOpenQuotientMap_mk.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
    exact continuous_mk.comp continuous_mul
  continuous_inv := continuous_inv.quotient_map' _

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