Theorems · Theorem · logic and foundations

FirstOrder.Language.LHom.onTerm.eq_def

∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L →ᴸ L') (x : L.Term α),
  φ.onTerm x =
    match x with
    | FirstOrder.Language.var i => FirstOrder.Language.var i
    | FirstOrder.Language.func f ts => FirstOrder.Language.func (φ.onFunction f) fun i => φ.onTerm (ts i)

Defined in

Mathlib.ModelTheory.Syntax

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms