monotone_chain_condition' — Mathlib

English

In a well-founded GT order, the monotone chain condition for a given a: ℕ → α holds: there exists n such that for all m≥n, a(n) ≥ a(m).

Русский

В хорошо основанном порядке GT выполняется монотонная цепная условность: существует n такое, что для всех m≥n выполняется a(n) ≥ a(m).

LaTeX

$$$$\exists n, \forall m, n \le m \rightarrow a(n) \ge a(m).$$$$

Lean4

theorem monotone_chain_condition' [Preorder α] [h : WellFoundedGT α] (a : ℕ →o α) : ∃ n, ∀ m, n ≤ m → ¬a n < a m :=
  wellFoundedGT_iff_monotone_chain_condition'.1 h a

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