English
If f has locally bounded variation on s, then for a ≤ b, variationOnFromTo f s a b = 0 iff every pair x,y in s ∩ Icc a b has edist (f x) (f y) = 0.
Русский
Если f имеет локальную ограниченность вариации на s и a ≤ b, то variationOnFromTo f s a b = 0 эквивалентно тому, что для всех x,y в s ∩ Icc a b расстояние edist (f x) (f y) = 0.
LaTeX
$$variationOnFromTo f s a b = 0 ↔ ∀ x ∈ s ∩ Icc a b, ∀ y ∈ s ∩ Icc a b, edist (f x) (f y) = 0$$
Lean4
protected theorem eq_zero_iff_of_le {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b : α} (ha : a ∈ s)
(hb : b ∈ s) (ab : a ≤ b) :
variationOnFromTo f s a b = 0 ↔ ∀ ⦃x⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0 :=
by
rw [variationOnFromTo.eq_of_le _ _ ab, ENNReal.toReal_eq_zero_iff, or_iff_left (hf a b ha hb),
eVariationOn.eq_zero_iff]
