English
A 1-dimensional version of definability for sets in M expresses that a subset s ⊆ M is definable exactly when the set of 1-length sequences whose first coordinate lies in s is definable in the same language.
Русский
1-мерная версия определения определимости для наборов в M говорит: множество s ⊆ M определимо тогда и только тогда, когда множество последовательностей длины 1, чья первая координата лежит в s, определимо тем же языком.
LaTeX
$$$\text{Definable}_L^{(1)}(s) := A\text{ Definable }L\{x:\mathrm{Fin}(1)\to M \mid x(0)\in s\}.$$$
Lean4
/-- A 1-dimensional version of `Definable`, for `Set M`. -/
def Definable₁ (s : Set M) : Prop :=
A.Definable L {x : Fin 1 → M | x 0 ∈ s}
