English
For a BV on s in a metric space, the distance dist(f x, f y) is bounded by (eVariationOn f s).toReal for x,y ∈ s.
Русский
Для BV на s в метрическом пространстве расстояние dist(f x, f y) ограничено Real частью eVariationOn f s для x,y ∈ s.
LaTeX
$$$\forall x,y\in s,\; dist(f x,f y) \le (eVariationOn f s).toReal$$
Lean4
theorem _root_.BoundedVariationOn.dist_le {E : Type*} [PseudoMetricSpace E] {f : α → E} {s : Set α}
(h : BoundedVariationOn f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : dist (f x) (f y) ≤ (eVariationOn f s).toReal :=
by
rw [← ENNReal.ofReal_le_ofReal_iff ENNReal.toReal_nonneg, ENNReal.ofReal_toReal h, ← edist_dist]
exact edist_le f hx hy