finite_of_compact_of_discrete — Mathlib

English

A space that is both compact and discrete is finite.

Русский

Пространство, одновременно компактное и дискретное, конечно.

LaTeX

$$$\\text{CompactSpace}(X) \\wedge \\text{DiscreteTopology}(X) \\Rightarrow \\text{Finite}(X)$$$

Lean4

/-- A compact discrete space is finite. -/
theorem finite_of_compact_of_discrete [CompactSpace X] [DiscreteTopology X] : Finite X :=
  Finite.of_finite_univ <| isCompact_univ.finite_of_discrete

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