monotoneOn — Mathlib

English

If f has locally bounded variation on s, then the function a ↦ variationOnFromTo f s a is monotone on s.

Русский

Если у f локальная ограниченность вариации на s, тогда a ↦ variationOnFromTo f s a монотонна на s.

LaTeX

$$MonotoneOn (variationOnFromTo f s a) s$$

Lean4

protected theorem monotoneOn (hf : LocallyBoundedVariationOn f s) {a : α} (as : a ∈ s) :
    MonotoneOn (variationOnFromTo f s a) s := by
  rintro b bs c cs bc
  rw [← variationOnFromTo.add hf as bs cs]
  exact le_add_of_nonneg_right (variationOnFromTo.nonneg_of_le f s bc)

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