monotone_chain_condition — Mathlib

English

For a partial order α, WellFoundedGT α implies a monotone chain condition for order-homomorphisms a: Nat → α; more precisely, there exists n with a(n) = a(m) for all m≥n.

Русский

Для частичного порядка α условие хорошего основания GT приводит к монотонной цепной условности для отображения a: Nat → α: существует n, такое что для всех m≥n выполняется a(n)=a(m).

LaTeX

$$$$\forall a:\, \mathrm{OrderHom}\; Nat \ α,\ \exists n, \forall m, n \le m \rightarrow a(n)=a(m).$$$$

Lean4

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

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