English
For Encodable types, a constructive version of the axiom of choice holds: from a family of nonempty choices, one can select a function picking a witness for each x.
Русский
Для кодируемых типов выполняется конструктивная версия аксиомы выбора: из каждой подсемей непустых множеств можно выбрать отображение, дающее свидетеля для каждого x.
LaTeX
$$$ (\forall x, \exists y, R x y) \Rightarrow \exists f: \forall x, \beta x, \forall x, R x (f x) $$$
Lean4
/-- A constructive version of `Classical.axiom_of_choice` for `Encodable` types. -/
theorem axiom_of_choice {α : Type*} {β : α → Type*} {R : ∀ x, β x → Prop} [∀ a, Encodable (β a)]
[∀ x y, Decidable (R x y)] (H : ∀ x, ∃ y, R x y) : ∃ f : ∀ a, β a, ∀ x, R x (f x) :=
⟨fun x => choose (H x), fun x => choose_spec (H x)⟩
