English
If hf is LocallyBoundedVariationOn f s, then for a fixed b ∈ s, the function a ↦ variationOnFromTo f s a b is antitone on s.
Русский
Если hf — локально ограниченная вариация, то фиксированная точка b образует антимонотонную функцию по a на s.
LaTeX
$$AntitoneOn (fun a => variationOnFromTo f s a b) s$$
Lean4
protected theorem antitoneOn (hf : LocallyBoundedVariationOn f s) {b : α} (bs : b ∈ s) :
AntitoneOn (fun a => variationOnFromTo f s a b) s :=
by
rintro a as c cs ac
dsimp only
rw [← variationOnFromTo.add hf as cs bs]
exact le_add_of_nonneg_left (variationOnFromTo.nonneg_of_le f s ac)