locallyBoundedVariationOn — Mathlib

English

A Lipschitz map f: ℝ → E has locally bounded variation on every subset.

Русский

Липшицева функция f: ℝ → E имеет локально ограниченную вариацию на любом подмножстве.

LaTeX

$$$ (hf : LipschitzWith C f) (s : Set\,\mathbb{R}) \Rightarrow LocallyBoundedVariationOn\ f\ s $$$

Lean4

theorem locallyBoundedVariationOn {f : ℝ → E} {C : ℝ≥0} (hf : LipschitzWith C f) (s : Set ℝ) :
    LocallyBoundedVariationOn f s :=
  hf.lipschitzOnWith.locallyBoundedVariationOn

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