antitoneOn — Mathlib

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)

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