English
If s is nonempty, there exists a monotone sequence in s with a point in s at every stage.
Русский
Если s непусто, существует монотонная последовательность в s, каждая точка которой принадлежит s.
LaTeX
$$eVariationOn.nonempty_monotone_mem {s : Set α} (hs : s.Nonempty) : Nonempty { u // Monotone u ∧ ∀ i : ℕ, u i ∈ s }$$
Lean4
/-- The (extended-real-valued) variation of a function `f` on a set `s` inside a linear order is
the supremum of the sum of `edist (f (u (i+1))) (f (u i))` over all finite increasing
sequences `u` in `s`. -/
noncomputable def eVariationOn (f : α → E) (s : Set α) : ℝ≥0∞ :=
⨆ p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ i, u i ∈ s }, ∑ i ∈ Finset.range p.1, edist (f (p.2.1 (i + 1))) (f (p.2.1 i))
