dist_le — Mathlib

English

For bounded β, dist f g ≤ C iff for every x, dist(f(x), g(x)) ≤ C.

Русский

При ограниченном β, расстояние между f и g не превосходит C тогда и только тогда, когда для каждого x выполняется dist(f(x), g(x)) ≤ C.

LaTeX

$$$\mathrm{dist} f g \le C \iff \forall x, \mathrm{dist}(f(x), g(x)) \le C$$$

Lean4

theorem dist_le [BoundedSpace β] {f g : α →ᵤ β} {C : ℝ} (hC : 0 ≤ C) :
    dist f g ≤ C ↔ ∀ x, dist (toFun f x) (toFun g x) ≤ C := by
  simp_rw [dist_edist, ← ENNReal.le_ofReal_iff_toReal_le (edist_ne_top _ _) hC, edist_le]

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