monotonicSequenceLimit — Mathlib

English

The limit value of an eventually-constant monotone sequence a: ℕ → α is a at the index monotonicSequenceLimitIndex a.

Русский

Предел последовательности равен значению a на индексе monotonicSequenceLimitIndex a.

LaTeX

$$$$\text{monotonicSequenceLimit } a = a(\text{monotonicSequenceLimitIndex } a).$$$$

Lean4

/-- The constant value of an eventually-constant monotone sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a
partially-ordered type. -/
noncomputable def monotonicSequenceLimit [Preorder α] (a : ℕ →o α) :=
  a (monotonicSequenceLimitIndex a)

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