isCompact_iff_finite — Mathlib

English

Let X be a space with the discrete topology. Then a subset s is compact iff s is finite.

Русский

Пусть X — дискретное пространство. Тогда множество s компактно тогда и только тогда, когда конечное.

LaTeX

$$$\operatorname{IsCompact}(s) \iff \#s < \infty$$$

Lean4

theorem isCompact_iff_finite [DiscreteTopology X] : IsCompact s ↔ s.Finite :=
  ⟨fun h => h.finite_of_discrete, fun h => h.isCompact⟩

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