English
If every finite set t admits some c with P(c,t), then there exists a sequence u: N → γ such that for every n, P(u(n), u'' Iio n).
Русский
Если для каждой конечной множества t существует элемент c, связанный с t, то существует последовательность u: N → γ такая, что для каждого n выполняется P(u(n), u'' Iio n).
LaTeX
$$$ (\\forall t : Set γ, t.Finite \\rightarrow \\exists c, P c t) \\rightarrow \\exists u : \\mathbb{N} \\to γ, \\forall n, P (u n) (u '' Iio n) $$$
Lean4
/-- If `P` is some relation between terms of `γ` and sets in `γ`, such that every finite set
`t : Set γ` has some `c : γ` related to it, then there is a recursively defined sequence `u` in `γ`
so `u n` is related to the image of `{0, 1, ..., n-1}` under `u`.
(We use this later to show sequentially compact sets are totally bounded.)
-/
theorem seq_of_forall_finite_exists {γ : Type*} {P : γ → Set γ → Prop} (h : ∀ t : Set γ, t.Finite → ∃ c, P c t) :
∃ u : ℕ → γ, ∀ n, P (u n) (u '' Iio n) :=
by
haveI : Nonempty γ := (h ∅ finite_empty).nonempty
choose! c hc using h
set f : (n : ℕ) → (g : (m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k : Iio n => g k.1 k.2)
set u : ℕ → γ := fun n => Nat.strongRecOn' n f
refine ⟨u, fun n => ?_⟩
convert hc (u '' Iio n) ((finite_lt_nat _).image _)
rw [image_eq_range]
exact Nat.strongRecOn'_beta
