English
For any a,b,c with a,b,c ∈ s and s locally bounded variation, equality of variationOnFromTo f s a b and a c is equivalent to equality of variationOnFromTo f s b c with a left cancellation property.
Русский
При локально ограниченной вариации равенство вариаций слева эквивалентно равенству вариаций между соответствующими точками.
LaTeX
$$variationOnFromTo f s a b = variationOnFromTo f s a c ↔ variationOnFromTo f s b c = 0$$
Lean4
protected theorem eq_left_iff {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b c : α} (ha : a ∈ s)
(hb : b ∈ s) (hc : c ∈ s) : variationOnFromTo f s a b = variationOnFromTo f s a c ↔ variationOnFromTo f s b c = 0 :=
by simp only [← variationOnFromTo.add hf ha hb hc, left_eq_add]