edist_le_range_sum_of_edist_le — Mathlib

English

Analogous bound in ENNReal for edist along an Ico-range with stepwise upper bounds d(i).

Русский

Аналогичное ограничение в ENNReal для edist вдоль диапазона Ico с шаговыми верхними границами d(i).

LaTeX

$$$\forall f:\mathbb{N} \to \alpha, {m,n},\; (m\le n)\Rightarrow edist(f(m), f(n)) \le \sum_{i=m}^{n-1} d(i),$ где каждый d(i) надлежащим образом ограничен.$$

Lean4

/-- A version of `edist_le_range_sum_edist` with each intermediate distance replaced
with an upper estimate. -/
theorem edist_le_range_sum_of_edist_le {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ≥0∞}
    (hd : ∀ {k}, k < n → edist (f k) (f (k + 1)) ≤ d k) : edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i :=
  Nat.Ico_zero_eq_range ▸ edist_le_Ico_sum_of_edist_le (zero_le n) fun _ => hd

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