le_monotonicSequenceLimit — Mathlib

English

If a is a monotone sequence under a Preorder with WellFoundedGT, then for every m, a(m) ≤ monotonicSequenceLimit a.

Русский

Если a — монотонная последовательность в предorder с WellFoundedGT, тогда для любого m имеет место a(m) ≤ monotonicSequenceLimit a.

LaTeX

$$$$\forall m,\ a(m) \le \mathrm{monotonicSequenceLimit}(a).$$$$

Lean4

theorem le_monotonicSequenceLimit [PartialOrder α] [WellFoundedGT α] (a : ℕ →o α) (m : ℕ) :
    a m ≤ monotonicSequenceLimit a :=
  by
  rcases le_or_gt m (monotonicSequenceLimitIndex a) with hm | hm
  · exact a.monotone hm
  · obtain h := WellFoundedGT.monotone_chain_condition a
    exact (Nat.sInf_mem (s := {n | ∀ m, n ≤ m → a n = a m}) h m hm.le).ge

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