hasLocallyBoundedVariationOn — Mathlib

English

If a function f has constant speed on s, then it has locally bounded variation on s; i.e., its variation on any compact subinterval is finite.

Русский

Если функция f имеет постоянную скорость на наборе s, то она имеет локально ограниченную вариацию на s; то есть вариация на любом ограниченном промежутке конечна.

LaTeX

$$HasConstantSpeedOnWith f s l ⇒ LocallyBoundedVariationOn f s$$

Lean4

theorem hasLocallyBoundedVariationOn (h : HasConstantSpeedOnWith f s l) : LocallyBoundedVariationOn f s :=
  fun x y hx hy => by simp only [BoundedVariationOn, h hx hy, Ne, ENNReal.ofReal_ne_top, not_false_iff]

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