isBounded_iff_eventually — Mathlib

English

Boundedness of s is equivalent to the eventual boundedness of distances: there exists an eventual bound C such that dist x y ≤ C for all x,y ∈ s.

Русский

Ограниченность s эквивалентна предельной ограниченности расстояний: существует предел C, такой что dist x y ≤ C для всех x,y ∈ s.

LaTeX

$$$ IsBounded(s) \iff \text{Eventually }(C \mapsto \forall x\in s\forall y\in s, dist(x,y) \le C) \text{ atTop}$$$

Lean4

theorem isBounded_iff_eventually {s : Set α} :
    IsBounded s ↔ ∀ᶠ C in atTop, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C :=
  isBounded_iff.trans
    ⟨fun ⟨C, h⟩ => eventually_atTop.2 ⟨C, fun _C' hC' _x hx _y hy => (h hx hy).trans hC'⟩, Eventually.exists⟩

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