instLocallyCompactSpace — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance instLocallyCompactSpace [LocallyCompactSpace M] : LocallyCompactSpace Mᵐᵒᵖ :=
  opHomeomorph.symm.isClosedEmbedding.locallyCompactSpace

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