English
The least index n at which a monotone sequence a: ℕ → α becomes constant from then on, defined via a lower bound of indices with a(n) = a(m) for all m≥n.
Русский
Наименьший индекс n, после которого монотонная последовательность a: ℕ → α становится постоянной; определяется как наименьшее n, удовлетворяющее ∀m≥n, a(n)=a(m).
LaTeX
$$$$\text{monotonicSequenceLimitIndex } a \;=\; \inf\{n : \forall m, n \le m \Rightarrow a(n)=a(m)\}.$$$$
Lean4
/-- Given an eventually-constant monotone sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a partially-ordered
type, `monotonicSequenceLimitIndex a` is the least natural number `n` for which `aₙ` reaches the
constant value. For sequences that are not eventually constant, `monotonicSequenceLimitIndex a`
is defined, but is a junk value. -/
noncomputable def monotonicSequenceLimitIndex [Preorder α] (a : ℕ →o α) : ℕ :=
sInf {n | ∀ m, n ≤ m → a n = a m}
