sum_le_of_monotoneOn_Iic — Mathlib

English

Analogous bound holds for monotoneOn_Iic (i in 0..n-1).

Русский

Аналогично ограничение для монотонной последовательности на Iic.

LaTeX

$$$\forall f:α\to E,\;\forall s,\;\forall n:\\mathbb{N},\; u:\mathbb{N}\to α \\; (\text{MonotoneOn }u(Iic\,n)) \\; (\forall i\le n, u(i)\in s) \\Rightarrow \sum_{i=0}^{n-1} edist(f(u(i+1)), f(u(i))) \le eVariationOn f s$$

Lean4

theorem sum_le_of_monotoneOn_Iic (f : α → E) {s : Set α} {n : ℕ} {u : ℕ → α} (hu : MonotoneOn u (Iic n))
    (us : ∀ i ≤ n, u i ∈ s) : (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) ≤ eVariationOn f s := by
  simpa using sum_le_of_monotoneOn_Icc f (m := 0) (hu.mono Icc_subset_Iic_self) fun i hi ↦ us i hi.2

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