English
Under a symmetric relation r, and the same finite-set existence hypothesis, there exists f: ℕ → α with ∀ n, P (f n) and Pairwise (r on f).
Русский
При симметричном отношении r и той же гипотезе существования над конечными множествами существует функция f: ℕ → α такая, что ∀ n, P (f n) и пары элементов удовлетворяют r.
LaTeX
$$$$ \\exists f : \\mathbb{N} \\to α, (\\forall n, P (f n)) \\wedge \\operatorname{Pairwise} (r \\text{ on } f). $$$$
Lean4
/-- Induction principle to build a sequence, by adding one point at a time satisfying a given
symmetric relation with respect to all the previously chosen points.
More precisely, Assume that, for any finite set `s`, one can find another point satisfying
some relation `r` with respect to all the points in `s`. Then one may construct a
function `f : ℕ → α` such that `r (f m) (f n)` holds whenever `m ≠ n`.
We also ensure that all constructed points satisfy a given predicate `P`. -/
theorem exists_seq_of_forall_finset_exists' {α : Type*} (P : α → Prop) (r : α → α → Prop) [IsSymm α r]
(h : ∀ s : Finset α, (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y) :
∃ f : ℕ → α, (∀ n, P (f n)) ∧ Pairwise (r on f) :=
by
rcases exists_seq_of_forall_finset_exists P r h with ⟨f, hf, hf'⟩
refine ⟨f, hf, fun m n hmn => ?_⟩
rcases lt_trichotomy m n with (h | rfl | h)
· exact hf' m n h
· exact (hmn rfl).elim
· unfold Function.onFun
apply symm
exact hf' n m h
