isBounded_iff_exists_ge — Mathlib

English

For a fixed real number c, s is bounded if and only if there exists C with c ≤ C such that for all x,y ∈ s, dist x y ≤ C.

Русский

Для заданного числа c существует C с c ≤ C и для всех x,y ∈ s выполняется dist(x,y) ≤ C, если s ограничено.

LaTeX

$$$ IsBounded(s) \iff ∃ C, c ≤ C ∧ ∀ x \in s, ∀ y \in s, dist(x,y) ≤ C $$$

Lean4

theorem isBounded_iff_exists_ge {s : Set α} (c : ℝ) :
    IsBounded s ↔ ∃ C, c ≤ C ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C :=
  ⟨fun h => ((eventually_ge_atTop c).and (isBounded_iff_eventually.1 h)).exists, fun h =>
    isBounded_iff.2 <| h.imp fun _ => And.right⟩

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