Theorems · Definition · logic and foundations

Set.TermDefinable

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

A function from a Cartesian power of a structure to that structure is term-definable over a set A when the value of the function is given by a term with constants A.

Defined in

Mathlib.ModelTheory.Definability

Cited by

12 results in Mathlib

Foundations

Depth 19 from the axioms · uses no axioms

Assumes

FirstOrder.Language.Structure