isCompact_iff_compactSpace — Mathlib

English

For any subset s of a topological space X, s is compact if and only if the subspace s is a compact space (CompactSpace s).

Русский

Для подмножества s пространства X выполняется: s компактно тогда, когда подпространство s является компактным пространством (CompactSpace s).

LaTeX

$$$\IsCompact(s) \iff \CompactSpace\,s$$$

Lean4

theorem isCompact_iff_compactSpace : IsCompact s ↔ CompactSpace s :=
  isCompact_iff_isCompact_univ.trans isCompact_univ_iff

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