eq_of_ge — Mathlib

English

For a real-valued f and φ monotone on t, the variation of the composed function on t equals the variation on φ(t) with arguments mapped by φ.

Русский

Для действительной функции f и монотонного φ на t вариация композиции равна вариации на образе φ(t) с учетом картирования φ.

LaTeX

$$variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)$$

Lean4

protected theorem eq_of_ge {a b : α} (h : b ≤ a) : variationOnFromTo f s a b = -(eVariationOn f (s ∩ Icc b a)).toReal :=
  by rw [variationOnFromTo.eq_neg_swap, neg_inj, variationOnFromTo.eq_of_le f s h]

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