self — Mathlib

English

If a ≤ b, then variationOnFromTo f s a b equals (eVariationOn f (s ∩ Icc a b)).toReal.

Русский

Если a ≤ b, то variationOnFromTo f s a b равно (eVariationOn f (s ∩ Icc a b)).toReal.

LaTeX

$$$\\text{variationOnFromTo}\\ f\\ s\\ a b = \\operatorname{toReal}(eVariationOn\\ f\\ (s \\cap Icc a b))$$$

Lean4

protected theorem self (a : α) : variationOnFromTo f s a a = 0 :=
  by
  dsimp only [variationOnFromTo]
  rw [if_pos le_rfl, Icc_self, eVariationOn.subsingleton, ENNReal.toReal_zero]
  exact fun x hx y hy => hx.2.trans hy.2.symm

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