edist_le — Mathlib

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

Похожие утверждения