isCompact_iff_isSeqCompact — Mathlib

English

For a uniform space X with a countably generated uniformity, CompactSpace X is equivalent to SeqCompactSpace X.

Русский

Для равномерного пространства X с счетно порождаемой равномерностью, компактное пространство эквивалентно последовательнос-кому пространству компактности.

LaTeX

$$$CompactSpace X \iff SeqCompactSpace X$ (under [UniformSpace X] and (uniformity X).IsCountablyGenerated).$$

Lean4

/-- A version of Bolzano-Weierstrass: in a uniform space with countably generated uniformity filter
(e.g., in a metric space), a set is compact if and only if it is sequentially compact. -/
protected theorem isCompact_iff_isSeqCompact : IsCompact s ↔ IsSeqCompact s :=
  ⟨fun H => H.isSeqCompact, fun H => H.isCompact⟩

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