allZFSetDefinable — Mathlib

English

All functions are classically definable: for any F : (Fin n → ZFSet) → ZFSet there is a Definable n F.

Русский

Во всех классических системах любая функция является определимой: для любой F : (Fin n → ZFSet) → ZFSet существует Definable n F.

LaTeX

$$$$ {n} \to (F : (Fin n → ZFSet) → ZFSet) \Rightarrow Definable n F. $$$$

Lean4

/-- All functions are classically definable. -/
noncomputable def allZFSetDefinable {n} (F : (Fin n → ZFSet.{u}) → ZFSet.{u}) : Definable n F where
  out xs := (F (mk <| xs ·)).out

Похожие утверждения