Theorems · Theorem · logic and foundations

Set.TermDefinable.comp

∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {β : Type u_1}
  {f : (α → M) → M} {g : α → (β → M) → M},
  A.TermDefinable L f → (∀ (i : α), A.TermDefinable L (g i)) → A.TermDefinable L fun b => f fun x => g x b

A k-ary TermDefinable function composed with k TermDefinable others is TermDefinable.

Defined in

Mathlib.ModelTheory.Definability

Cited by

2 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.Structure