isBounded_of_bddAbove_of_bddBelow

English

In a space with a conditionally complete linear order compatible with the metric, any order-bounded set is metric-bounded.

Русский

В пространстве с условно полным линейным порядком, совместимым с метрикой, множество, ограниченное по порядку, ограничено по метрике.

LaTeX

$$$IsBounded(s)\\Leftarrow (BddAbove(s)\\land BddBelow(s)).$$$

Lean4

/-- In a pseudo metric space with a conditionally complete linear order such that the order and the
metric structure give the same topology, any order-bounded set is metric-bounded. -/
theorem isBounded_of_bddAbove_of_bddBelow {s : Set α} (h₁ : BddAbove s) (h₂ : BddBelow s) : IsBounded s :=
  let ⟨u, hu⟩ := h₁
  let ⟨l, hl⟩ := h₂
  (isBounded_Icc l u).subset (fun _x hx => mem_Icc.mpr ⟨hl hx, hu hx⟩)

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