closure — Mathlib

English

The closure of a compact set in an R1 space is compact: If K is compact, then closure(K) is compact.

Русский

Замыкание компактного множества в R1-пространстве компактно: если K компактно, то closure(K) компактно.

LaTeX

$$IsCompact(closure(K))$$

Lean4

/-- The closure of a compact set in an R₁ space is a compact set. -/
protected theorem closure {K : Set X} (hK : IsCompact K) : IsCompact (closure K) :=
  by
  refine isCompact_of_finite_subcover fun U hUo hKU ↦ ?_
  rcases hK.elim_finite_subcover U hUo (subset_closure.trans hKU) with ⟨t, ht⟩
  exact ⟨t, hK.closure_subset_of_isOpen (isOpen_biUnion fun _ _ ↦ hUo _) ht⟩

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