instLocallyCompactSpace — Mathlib

English

If G is locally compact and N is a subgroup, then the quotient G/N is locally compact.

Русский

Если G локально компактна и N является подгруппой, то G/N локально компактна.

LaTeX

$$$\operatorname{LocallyCompactSpace}(G) \Rightarrow \operatorname{LocallyCompactSpace}(G/N).$$$

Lean4

/-- A quotient of a locally compact group is locally compact. -/
@[to_additive]
instance instLocallyCompactSpace [LocallyCompactSpace G] (N : Subgroup G) : LocallyCompactSpace (G ⧸ N) :=
  QuotientGroup.isOpenQuotientMap_mk.locallyCompactSpace

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