English
If for every x in a filter l there exists y with r(x,y), then there exists a function f choosing such y for almost all x with respect to l.
Русский
Если для каждого x в фильтре l существует y с свойством r(x,y), то существует функция f, выбирающая такой y для большинства x по отношению к l.
LaTeX
$$$\\Big(\\forall^{\\!\\text{freq}} x\\in l\\;\\exists y:\\ r(x,y)\\Big) \\Rightarrow \\exists f:\\alpha\\to\\beta,\\ \\forall^{\\!\\text{freq}} x\\in l\\; r(x,f(x))$$$
Lean4
theorem choice {r : α → β → Prop} {l : Filter α} [l.NeBot] (h : ∀ᶠ x in l, ∃ y, r x y) :
∃ f : α → β, ∀ᶠ x in l, r x (f x) :=
by
haveI : Nonempty β :=
let ⟨_, hx⟩ := h.exists;
hx.nonempty
choose! f hf using fun x (hx : ∃ y, r x y) => hx
exact ⟨f, h.mono hf⟩
