instWeaklyLocallyCompactSpace — Mathlib

English

If M is weakly locally compact, then DomMulAct M is weakly locally compact.

Русский

Если M слабо локально компактно, то DomMulAct M слабо локально компактно.

LaTeX

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

Lean4

@[to_additive]
instance instWeaklyLocallyCompactSpace [WeaklyLocallyCompactSpace M] : WeaklyLocallyCompactSpace Mᵈᵐᵃ :=
  isClosedEmbedding_mk_symm.weaklyLocallyCompactSpace

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