English
For a preorder α, WellFoundedGT α is equivalent to a monotone chain condition: every increasing order-homomorphism a: ℕ → α eventually becomes constant along a tail.
Русский
Для предоргана α условие WellFoundedGT эквивалентно монотонной цепной условности: каждый монотонный отображение a: ℕ → α в конце становится константным.
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
/-- The **monotone chain condition**: a preorder is co-well-founded iff every increasing sequence
contains two non-increasing indices.
See `wellFoundedGT_iff_monotone_chain_condition` for a stronger version on partial orders. -/
theorem wellFoundedGT_iff_monotone_chain_condition' [Preorder α] :
WellFoundedGT α ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → ¬a n < a m :=
by
refine ⟨fun h a => ?_, fun h => ?_⟩
· obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.wf.has_min _ (Set.range_nonempty a)
exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩
· rw [WellFoundedGT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]
refine ⟨fun a => ?_⟩
obtain ⟨n, hn⟩ := h (a.swap : _ →r _).toOrderHom
exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)
