Theorems · Theorem · logic and foundations

Set.TermDefinable.const

∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁}
  (C : (L.withConstants ↑A).Constants), A.TermDefinable L (Function.const (α → M) ↑C)

Constant functions are TermDefinable, assuming the constant value is a language constant.

Defined in

Mathlib.ModelTheory.Definability

Cited by

1 results in Mathlib

Foundations

Depth 20 from the axioms · uses Quot.sound

Assumes

FirstOrder.Language.Structure