instLocallyCompactSpace — Mathlib

English

If M is locally compact, then the DomMulAct space Mᵈᵐᵃ is locally compact.

Русский

Если M локально компактно, то Mᵈᵐᵃ локально компактно.

LaTeX

$$$$ \operatorname{LocallyCompactSpace}(M) \Rightarrow \operatorname{LocallyCompactSpace}(\mathrm{DomMulAct}(M)) $$$$

Lean4

@[to_additive]
instance instLocallyCompactSpace [LocallyCompactSpace M] : LocallyCompactSpace Mᵈᵐᵃ :=
  isOpenEmbedding_mk_symm.locallyCompactSpace

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