English
A global witness exists for a family of local witnesses: if every index i has a witness b_i with P(i,b_i), then there is a function b assigning to each i such that P(i,b(i)) holds frequently along the filter.
Русский
Существование глобального свидетеля, который выбирает по каждому индексу i подходящее значение b(i) с выполняющимся свойством.
LaTeX
$$$\\left(\\forall i,\\mathrm{Nonempty}(\\alpha(i))\\right)\\!\\;\\Rightarrow\\;\\left(\\forall\\! F:\\text{Filter } i,\\ \\forall i:\\ \\exists b_i:\\ P(i,b_i)\\right)\\iff \\exists b: \\Pi i, \\alpha(i),\\ \\forall i:\\ P(i,b(i))$$$
Lean4
theorem skolem {ι : Type*} {α : ι → Type*} [∀ i, Nonempty (α i)] {P : ∀ i : ι, α i → Prop} {F : Filter ι} :
(∀ᶠ i in F, ∃ b, P i b) ↔ ∃ b : (Π i, α i), ∀ᶠ i in F, P i (b i) := by
classical
refine ⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩
refine ⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩
filter_upwards [H] with i hi
exact dif_pos hi ▸ hi.choose_spec
