sub_le — Mathlib

English

For a BV on s in a real-valued setting, f x - f y ≤ (eVariationOn f s).toReal for x,y ∈ s.

Русский

Для BV на s в вещественном пространстве f(x) - f(y) ≤ V_s(f) для x,y ∈ s.

LaTeX

$$$\forall x,y\in s,\; f(x)-f(y) \le (eVariationOn f s).toReal$$

Lean4

theorem _root_.BoundedVariationOn.sub_le {f : α → ℝ} {s : Set α} (h : BoundedVariationOn f s) {x y : α} (hx : x ∈ s)
    (hy : y ∈ s) : f x - f y ≤ (eVariationOn f s).toReal :=
  by
  apply (le_abs_self _).trans
  rw [← Real.dist_eq]
  exact h.dist_le hx hy

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