English
If two functions f and f' have zero distance pointwise on a set s, then their e-variation on s coincides: eVariationOn(f, s) = eVariationOn(f', s).
Русский
Если две функции f и f' удовлетворяют условию edist(f x, f'(x)) = 0 для всех x ∈ s, то их e-variation на s совпадает: eVariationOn(f, s) = eVariationOn(f', s).
LaTeX
$$$\forall f,f',s\left(\forall x\,(x\in s \rightarrow \operatorname{edist}(f x,f' x)=0)\right)\Rightarrow eVariationOn f s = eVariationOn f' s$$
Lean4
theorem eq_of_edist_zero_on {f f' : α → E} {s : Set α} (h : ∀ ⦃x⦄, x ∈ s → edist (f x) (f' x) = 0) :
eVariationOn f s = eVariationOn f' s := by
dsimp only [eVariationOn]
congr 1 with p : 1
congr 1 with i : 1
rw [edist_congr_right (h <| p.snd.prop.2 (i + 1)), edist_congr_left (h <| p.snd.prop.2 i)]