English
General equivalence: if LocallyBoundedVariationOn f s holds, then for any a,b, variationOnFromTo f s a b = 0 is equivalent to a universal edist condition on all x,y in s ∩ uIcc a b.
Русский
Обобщённая эквивалентность: если LocallyBoundedVariationOn f s выполняется, то variationOnFromTo f s a b = 0 эквивалентно всем x,y в s ∩ uIcc a b удовлетворяют edist (f x) (f y) = 0.
LaTeX
$$variationOnFromTo f s a b = 0 ↔ ∀ x ∈ s ∩ uIcc a b, ∀ y ∈ s ∩ uIcc a b, edist (f x) (f y) = 0$$
Lean4
protected theorem eq_zero_iff {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b : α} (ha : a ∈ s)
(hb : b ∈ s) :
variationOnFromTo f s a b = 0 ↔
∀ ⦃x⦄ (_hx : x ∈ s ∩ uIcc a b) ⦃y⦄ (_hy : y ∈ s ∩ uIcc a b), edist (f x) (f y) = 0 :=
by
rcases le_total a b with (ab | ba)
· rw [uIcc_of_le ab]
exact variationOnFromTo.eq_zero_iff_of_le hf ha hb ab
· rw [uIcc_of_ge ba]
exact variationOnFromTo.eq_zero_iff_of_ge hf ha hb ba
