isBounded_iff_nndist — Mathlib

English

The boundedness of s is equivalent to the existence of a nonnegative real C such that for all x,y ∈ s, their nndist is at most C.

Русский

Ограниченность множества s эквивалентна наличию C ∈ ℝ≥0 с nndist(x,y) ≤ C для всех x,y ∈ s.

LaTeX

$$$ IsBounded(s) \iff ∃ C \in ℝ_{≥0}, \forall x \in s, \forall y \in s, \operatorname{nndist}(x,y) ≤ C $$$

Lean4

theorem isBounded_iff_nndist {s : Set α} : IsBounded s ↔ ∃ C : ℝ≥0, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → nndist x y ≤ C := by
  simp only [isBounded_iff_exists_ge 0, NNReal.exists, ← NNReal.coe_le_coe, ← dist_nndist, NNReal.coe_mk, exists_prop]

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