partiallyWellOrderedOn — Mathlib

English

For any s, r, s is PWOn by r if and only if every sequence in s contains a pair of indices m < n with r(f(m), f(n)).

Русский

Для любых s, r, s частично хорошо упорядочено по r тогда и только тогда, когда любая последовательность в s содержит пару индексов m < n с r(f(m), f(n)).

LaTeX

$$$(s.PartiallyWellOrderedOn r) \\iff \\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

@[nontriviality]
theorem partiallyWellOrderedOn (hs : s.Subsingleton) : PartiallyWellOrderedOn s r :=
  hs.finite.partiallyWellOrderedOn

Похожие утверждения