English
A constructive version of Skolemization for Encodable types: from ∀ x, ∃ y, P x y we obtain ∃ f, ∀ x, P x (f x).
Русский
Конструктивная версия сколема для кодируемых типов: из ∀ x ∃ y P(x,y) следует ∃ f, ∀ x P(x, f(x)).
LaTeX
$$$ (\forall x, \exists y, P(x,y)) \iff \exists f: \forall x, \beta x, \forall x, P(x, f x) $$$
Lean4
/-- A constructive version of `Classical.skolem` for `Encodable` types. -/
theorem skolem {α : Type*} {β : α → Type*} {P : ∀ x, β x → Prop} [∀ a, Encodable (β a)] [∀ x y, Decidable (P x y)] :
(∀ x, ∃ y, P x y) ↔ ∃ f : ∀ a, β a, ∀ x, P x (f x) :=
⟨axiom_of_choice, fun ⟨_, H⟩ x => ⟨_, H x⟩⟩
/-
There is a total ordering on the elements of an encodable type, induced by the map to ℕ.
-/
