eq_left_iff — Mathlib

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]

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