Theorems · Theorem · logic and foundations

FirstOrder.Language.Term.relabel.eq_def

∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (g : α → β) (x : L.Term α),
  FirstOrder.Language.Term.relabel g x =
    match x with
    | FirstOrder.Language.var i => FirstOrder.Language.var (g i)
    | FirstOrder.Language.func f ts => FirstOrder.Language.func f fun {i} => FirstOrder.Language.Term.relabel g (ts i)

Defined in

Mathlib.ModelTheory.Syntax

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms