partiallyWellOrderedOn_iff_exists_lt

English

For every relation r and subset s, s is partially well-ordered by r if and only if every sequence of elements of s has two indices in increasing order that are related by r.

Русский

Для любой пары отношения и подмножестве s, s частично хорошо упорядовано по r тогда и только тогда, когда каждая последовательность элементов s имеет две позиции с возрастанием индексов, которые связаны отношением r.

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

theorem partiallyWellOrderedOn_iff_exists_lt :
    s.PartiallyWellOrderedOn r ↔ ∀ f : ℕ → α, (∀ n, f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n) :=
  ⟨PartiallyWellOrderedOn.exists_lt, fun hf f ↦ hf _ fun n ↦ (f n).2⟩

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