locallyBoundedVariationOn — Mathlib

English

A LipschitzOnWith map f: ℝ → E on s has locally bounded variation on s.

Русский

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

LaTeX

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

Lean4

theorem locallyBoundedVariationOn {f : ℝ → E} {C : ℝ≥0} {s : Set ℝ} (hf : LipschitzOnWith C f s) :
    LocallyBoundedVariationOn f s :=
  hf.comp_locallyBoundedVariationOn (mapsTo_id _) (@monotoneOn_id ℝ _ s).locallyBoundedVariationOn

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