English
If f has locally bounded variation on s, for b ≤ a, variationOnFromTo f s a b = 0 iff edist between any x,y in s ∩ Icc b a is zero after Real part conversion.
Русский
Если f локально ограничена вариация на s и b ≤ a, то variationOnFromTo f s a b = 0 эквивалентно нулю расстоянию между x,y в s ∩ Icc b a после отображения в Real.
LaTeX
$$variationOnFromTo f s a b = 0 ↔ ∀ x ∈ s ∩ Icc b a, ∀ y ∈ s ∩ Icc b a, edist (f x) (f y) = 0$$
Lean4
protected theorem eq_zero_iff_of_ge {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b : α} (ha : a ∈ s)
(hb : b ∈ s) (ba : b ≤ a) :
variationOnFromTo f s a b = 0 ↔ ∀ ⦃x⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0 :=
by
rw [variationOnFromTo.eq_of_ge _ _ ba, neg_eq_zero, ENNReal.toReal_eq_zero_iff, or_iff_left (hf b a hb ha),
eVariationOn.eq_zero_iff]
