isCompact — Mathlib

English

In a uniform space with a countably generated uniformity, a set is compact iff it is sequentially compact.

Русский

В равномерном пространстве с счетно порождаемой равномерностью множество компактно тогда и только тогда, когда оно последовательнос-но компактно.

LaTeX

$$$IsCompact s \iff IsSeqCompact s$ under [uniformity].IsCountablyGenerated.$$

Lean4

/-- If `𝓤 β` is countably generated, then any sequentially compact set is compact. -/
protected theorem isCompact (hs : IsSeqCompact s) : IsCompact s :=
  isCompact_iff_totallyBounded_isComplete.2 ⟨hs.totallyBounded, hs.isComplete⟩

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