toCompactSpace — Mathlib

English

The space s, viewed as a subspace of α, is compact whenever s is a compact subset of α.

Русский

Пространство s, рассматриваемое как подпространство α, компактно тогда и только тогда, когда s является компактным подмножеством α.

LaTeX

$$$ \text{CompactSpace}(s \text{ as a subspace of } \alpha) \quad \text{whenever} \quad s \text{ is compact in } \alpha. $$$$

Lean4

instance toCompactSpace {s : NonemptyCompacts α} : CompactSpace s :=
  isCompact_iff_compactSpace.1 s.isCompact

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