English
If x,y ∈ s, then edist(f x, f y) ≤ eVariationOn f s.
Русский
Если x,y ∈ s, то edist(f x, f y) ≤ eVariationOn f s.
LaTeX
$$$\forall f:α\to E,\; s\subset α,\; x,y\in s\Rightarrow edist(f x, f y) \le eVariationOn f s$$
Lean4
theorem edist_le (f : α → E) {s : Set α} {x y : α} (hx : x ∈ s) (hy : y ∈ s) : edist (f x) (f y) ≤ eVariationOn f s :=
by
wlog hxy : y ≤ x generalizing x y
· rw [edist_comm]
exact this hy hx (le_of_not_ge hxy)
let u : ℕ → α := fun n => if n = 0 then y else x
have hu : Monotone u :=
monotone_nat_of_le_succ fun
| 0 => hxy
| (_ + 1) => le_rfl
have us : ∀ i, u i ∈ s := fun
| 0 => hy
| (_ + 1) => hx
simpa only [Finset.sum_range_one] using sum_le f 1 hu us