English
For a partial order α, WellFoundedGT α holds iff every monotone increasing order-homomorphism a: ℕ → α eventually stabilizes, i.e., a(n) = a(m) for some tail.
Русский
Для частично упорядоченного множества α условие WellFoundedGT эквивалентно тому, что каждое возрастающее отображение a: ℕ → α стабилизируется на бесконечности: существует n, для всех m≥n выполняется a(n)=a(m).
LaTeX
$$$$\text{WellFoundedGT }\alpha \iff \forall a:\, \mathbb{N} \to_o \alpha,\ \exists n, \forall m, n \le m \rightarrow a(n)=a(m).$$$$
Lean4
/-- A stronger version of the **monotone chain** condition for partial orders.
See `wellFoundedGT_iff_monotone_chain_condition'` for a version on preorders. -/
theorem wellFoundedGT_iff_monotone_chain_condition [PartialOrder α] :
WellFoundedGT α ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → a n = a m :=
wellFoundedGT_iff_monotone_chain_condition'.trans <|
by
congrm ∀ a, ∃ n, ∀ m h, ?_
rw [lt_iff_le_and_ne]
simp [a.mono h]
