finite — Mathlib

English

If a subset s is compact and the subspace topology on s is discrete, then s is finite.

Русский

Если множество s компактно и подпространство s дискретно, то s конечно.

LaTeX

$$$\IsCompact\,s \land \DiscreteTopology\,s \Rightarrow s\text{ is finite}$; equivalently, $\#s < \infty$$$

Lean4

theorem finite (hs : IsCompact s) (hs' : DiscreteTopology s) : s.Finite :=
  finite_coe_iff.mp (@finite_of_compact_of_discrete _ _ (isCompact_iff_compactSpace.mp hs) hs')

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