DefinableSet — Mathlib

English

DefinableSet A α consists of all subsets s ⊆ (α → M) that are definable over A in the language L; that is, membership in s is given by a first-order formula with parameters from A.

Русский

DefinableSet A α состоит из всех подмножеств s ⊆ (α → M), которые определимы над A в языке L; то есть принадлежность к s задаётся формулой первого порядка с параметрами из A.

LaTeX

$$$$ \\mathrm{DefinableSet}(L,A) = \\{ s \\subseteq (\\alpha \\to M) \\mid A \\text{-Definable}_L(s) \\}. $$$$

Lean4

/-- Definable sets are subsets of finite Cartesian products of a structure such that membership is
  given by a first-order formula. -/
def DefinableSet :=
  { s : Set (α → M) // A.Definable L s }

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