isCompact_closure — Mathlib

English

For a finite set s in an R0 space, the closure of s is compact.

Русский

Для конечного множества s в R0-пространстве замыкание s компактно.

LaTeX

$$$s\\text{ finite} \\Rightarrow \\operatorname{IsCompact}(\\overline{s})$$$

Lean4

/-- In an R₀ space, the closure of a finite set is a compact set. -/
theorem isCompact_closure {s : Set X} (hs : s.Finite) : IsCompact (closure s) :=
  let _ : Bornology X := .relativelyCompact X
  Bornology.relativelyCompact.isBounded_iff.1 hs.isBounded

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