English
If (α, r) is a well-quasi-ordered set and s ⊆ α is an antichain with respect to r, then s is finite.
Русский
Если (α, r) образует хорошо упорядоченное множество, и s ⊆ α образует антицепь относительно r, то s конечна.
LaTeX
$$$\\forall \\alpha\\ (r:\\alpha \\to \\alpha \\to \\mathrm{Prop}),\\ \\forall s\\subseteq \\alpha,\\ \\mathrm{IsAntichain}(r,s) \\wedge \\mathrm{WellQuasiOrdered}(r) \\Rightarrow \\mathrm{Fin}(s)$$$
Lean4
theorem finite_of_wellQuasiOrdered {s : Set α} (hs : IsAntichain r s) (hr : WellQuasiOrdered r) : s.Finite :=
by
refine Set.not_infinite.1 fun hi => ?_
obtain ⟨m, n, hmn, h⟩ := hr fun n => hi.natEmbedding _ n
exact
hmn.ne
((hi.natEmbedding _).injective <|
Subtype.val_injective <| hs.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)
