English
A subset s of the function-type α → M is definable over a set A if there exists a formula φ in the expanded language L[[A]] such that s consists exactly of those α-tuples realizing φ.
Русский
Подмножество s ⊆ α → M определимо над множеством A, если существует формула φ в расширенном языке L[[A]], такая что s состоит ровно из тех α-куплетов, которые реализуют φ.
LaTeX
$$$\\\\exists \\\\varphi : L[[A]].Formula \\\\alpha, \\\\ s = \\\\{ v : \\\\alpha \to M \\\\mid \\\\varphi.Realize v \\\}$$$
Lean4
/-- A subset of a finite Cartesian product of a structure is definable over a set `A` when
membership in the set is given by a first-order formula with parameters from `A`. -/
def Definable (s : Set (α → M)) : Prop :=
∃ φ : L[[A]].Formula α, s = setOf φ.Realize
