English
For any f, natural n, an increasing sequence u with values in s, the sum of successive edists along the path is bounded by the e-variation on s: sum ≤ eVariationOn(f, s).
Русский
Для любого f, натурального n, возрастающей последовательности u с значениями в s сумма попарных расстояний вдоль траектории ограничена eVariationOn(f, s).
LaTeX
$$$\forall f:α\to E,\;\forall n:\mathbb{N},\;\forall u:\mathbb{N}\to α\\\; (\text{Monotone }u)\; (\forall i, u(i) \in s) \\Rightarrow \sum_{i=0}^{n-1} edist\big(f(u(i+1)), f(u(i))\big) \le eVariationOn f s$$
Lean4
theorem sum_le (f : α → E) {s : Set α} (n : ℕ) {u : ℕ → α} (hu : Monotone u) (us : ∀ i, u i ∈ s) :
(∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) ≤ eVariationOn f s :=
le_iSup_of_le ⟨n, u, hu, us⟩ le_rfl
