instWeaklyLocallyCompactSpaceMultiplicative

English

If X is weakly locally compact, then Multiplicative X is weakly locally compact.

Русский

Если X слабо локально компактно, то Multiplicative X слабо локально компактно.

LaTeX

$$$\operatorname{WeaklyLocallyCompactSpace}(X) \implies \operatorname{WeaklyLocallyCompactSpace}(\mathrm{Multiplicative}\,X)$$$

Lean4

instance [WeaklyLocallyCompactSpace X] : WeaklyLocallyCompactSpace (Multiplicative X) :=
  ‹WeaklyLocallyCompactSpace X›

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