isBounded_closure_of_isBounded — Mathlib

English

If s is bounded, then its closure is also bounded.

Русский

Если множество s ограничено, то его замыкание также ограничено.

LaTeX

$$IsBounded(s) → IsBounded(closure s)$$

Lean4

theorem isBounded_closure_of_isBounded (h : IsBounded s) : IsBounded (closure s) :=
  let ⟨C, h⟩ := isBounded_iff.1 h
  isBounded_iff.2 ⟨C, fun _a ha _b hb => isClosed_Iic.closure_subset <| map_mem_closure₂ continuous_dist ha hb h⟩

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