Theorems · Theorem · logic and foundations

Set.TermDefinable.trans

∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} {L' : FirstOrder.Language} [inst : L.Structure M]
  [inst_1 : L'.Structure M] {β : Type u_1} {f : (β → M) → M},
  A.TermDefinable L f →
    (∀ {n : ℕ} (g : (L.withConstants ↑A).Functions n),
        A.TermDefinable L' fun v => FirstOrder.Language.Term.realize v g.term) →
      A.TermDefinable L' f

TermDefinable is transitive. If f is TermDefinable in a structure S on L, and all of the functions' realizations on S are TermDefinable on a structure T on L', then f is TermDefinable on T in L'.

Defined in

Mathlib.ModelTheory.Definability

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure