isBounded — Mathlib

English

A totally bounded set is bounded.

Русский

Тотально ограниченное множество ограничено.

LaTeX

$$$TotallyBounded\; s \Rightarrow IsBounded\; s$$$

Lean4

/-- A totally bounded set is bounded -/
theorem _root_.TotallyBounded.isBounded {s : Set α} (h : TotallyBounded s) : IsBounded s :=
  -- We cover the totally bounded set by finitely many balls of radius 1,
    -- and then argue that a finite union of bounded sets is bounded

  let ⟨_t, fint, subs⟩ := (totallyBounded_iff.mp h) 1 zero_lt_one
  ((isBounded_biUnion fint).2 fun _ _ => isBounded_ball).subset subs

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