English
Let s be partially well-ordered by a relation r. Then for any sequence f with values in s, there exist m < n such that r(f(m), f(n)).
Русский
Пусть s частично хорошо упорядовано по отношению r. Тогда для любой последовательности f со значениями в s существует пара индексов m < n такая, что r(f(m), f(n)).
LaTeX
$$$s.PartiallyWellOrderedOn r \\to \\forall f:\\\\mathbb{N} \\to \\alpha, (\\forall n, f(n) \\in s) \\to \\exists m n, m < n \\land r(f(m), f(n))$$$
Lean4
/-- `s.PartiallyWellOrderedOn r` indicates that the relation `r` is `WellQuasiOrdered` when
restricted to `s`.
A set is partially well-ordered by a relation `r` when any infinite sequence contains two elements
where the first is related to the second by `r`. Equivalently, any antichain (see `IsAntichain`) is
finite, see `Set.partiallyWellOrderedOn_iff_finite_antichains`.
TODO: rename this to `WellQuasiOrderedOn` to match `WellQuasiOrdered`. -/
def PartiallyWellOrderedOn (s : Set α) (r : α → α → Prop) : Prop :=
WellQuasiOrdered (Subrel r (· ∈ s))
