closure — Mathlib

English

The closure of a totally bounded set is totally bounded.

Русский

ЗамыканиеTotallyBounded множества сохраняет свойство полного ограничения.

LaTeX

$$$$\\text{TotallyBounded}(s) \\Rightarrow TotallyBounded(\\overline{s}).$$$$

Lean4

/-- The closure of a totally bounded set is totally bounded. -/
theorem closure {s : Set α} (h : TotallyBounded s) : TotallyBounded (closure s) :=
  uniformity_hasBasis_closed.totallyBounded_iff.2 fun V hV =>
    let ⟨t, htf, hst⟩ := h V hV.1
    ⟨t, htf, closure_minimal hst <| htf.isClosed_biUnion fun _ _ => hV.2.preimage (.prodMk_left _)⟩

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