English
If s is IsPreorder and s is PWOn by r, then for every f: ℕ → α with values in s there exists a monotone subsequence of f.
Русский
Если s частично хорошо упорядочено по r и задано отношение порядка, тогда для любой f: ℕ → α с значениями в s существует мономонтная подпоследовательность f.
LaTeX
$$$s.PartiallyWellOrderedOn r \\to \\forall f:\\\\mathbb{N} \\to \\alpha, (\\\\forall n, f(n) \\in s) \\\\to \\exists g : \\\\mathbb{N} \\\\hookrightarrow \\\\mathbb{N}, \\forall m n:\\\\mathbb{N}, m \\le n \\to r (f (g m)) (f (g n))$$$
Lean4
theorem partiallyWellOrderedOn_iff_finite_antichains [IsSymm α r] :
s.PartiallyWellOrderedOn r ↔ ∀ t, t ⊆ s → IsAntichain r t → t.Finite :=
by
refine ⟨fun h t ht hrt => hrt.finite_of_partiallyWellOrderedOn (h.mono ht), ?_⟩
rw [partiallyWellOrderedOn_iff_exists_lt]
intro hs f hf
by_contra! H
refine infinite_range_of_injective (fun m n hmn => ?_) (hs _ (range_subset_iff.2 hf) ?_)
· obtain h | h | h := lt_trichotomy m n
· refine (H _ _ h ?_).elim
rw [hmn]
exact refl _
· exact h
· refine (H _ _ h ?_).elim
rw [hmn]
exact refl _
rintro _ ⟨m, hm, rfl⟩ _ ⟨n, hn, rfl⟩ hmn
obtain h | h := (ne_of_apply_ne _ hmn).lt_or_gt
· exact H _ _ h
· exact mt symm (H _ _ h)
