English
Given a predicate P and a relation r, if for every finite s ⊆ α there exists y with P y and r x y for all x ∈ s, then there exists f: ℕ → α with ∀ n, P (f n) and ∀ m < n, r (f m) (f n).
Русский
Если для каждого конечного подмножества s ⊆ α существует y с P y и r x y для всех x ∈ s, то существует f: ℕ → α такая, что ∀ n, P (f n) и ∀ m < n, r (f m) (f n).
LaTeX
$$$$ \\forall P \\forall r, (\\forall s : Finset α, (\\forall x ∈ s, P x) \\to \\exists y, P y \\wedge \\forall x ∈ s, r x y) \\Rightarrow \\exists f : \\mathbb{N} \\to α, (\\forall n, P (f n)) \\wedge \\forall m n, m < n \\to r (f m) (f n). $$$$
Lean4
/-- Induction principle to build a sequence, by adding one point at a time satisfying a given
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)
(h : ∀ s : Finset α, (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y) :
∃ f : ℕ → α, (∀ n, P (f n)) ∧ ∀ m n, m < n → r (f m) (f n) := by
classical
have : Nonempty α := by
rcases h ∅ (by simp) with ⟨y, _⟩
exact ⟨y⟩
choose! F hF using h
have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
set f := seqOfForallFinsetExistsAux P r h' with hf
have A : ∀ n : ℕ, P (f n) := by
intro n
induction n using Nat.strong_induction_on with
| _ n IH
have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
rw [hf, seqOfForallFinsetExistsAux]
exact
(Classical.choose_spec (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
(by simp [IH'])).1
refine ⟨f, A, fun m n hmn => ?_⟩
conv_rhs => rw [hf]
rw [seqOfForallFinsetExistsAux]
apply
(Classical.choose_spec (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩
