Theorems · Definition · logic and foundations

Set.Definable

{M : Type w} → Set M → (L : FirstOrder.Language) → [L.Structure M] → {α : Type u₁} → Set (α → M) → Prop

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.

Defined in

Mathlib.ModelTheory.Definability

Cited by

39 results in Mathlib

Foundations

Depth 22 from the axioms · uses Quot.sound

Assumes

FirstOrder.Language.Structure