exists_lt — Mathlib

English

For a set s and relation r, s is partially well-ordered by r if and only if every sequence of elements of s has two 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 \\leftrightarrow \\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 exists_lt (hs : s.PartiallyWellOrderedOn r) {f : ℕ → α} (hf : ∀ n, f n ∈ s) : ∃ m n, m < n ∧ r (f m) (f n) :=
  hs fun n ↦ ⟨_, hf n⟩

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