dist_le — Mathlib

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

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