instWeaklyLocallyCompactSpace — Mathlib

English

If M is WeaklyLocallyCompactSpace, then Mᵐᵒᵖ is WeaklyLocallyCompactSpace.

Русский

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

LaTeX

$$$$ \operatorname{WeaklyLocallyCompactSpace}(M) \Rightarrow \operatorname{WeaklyLocallyCompactSpace}(M^{\mathrm{op}}) $$$$

Lean4

@[to_additive]
instance instWeaklyLocallyCompactSpace [WeaklyLocallyCompactSpace M] : WeaklyLocallyCompactSpace Mᵐᵒᵖ :=
  opHomeomorph.symm.isClosedEmbedding.weaklyLocallyCompactSpace

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