Theorems · Definition · logic and foundations

FirstOrder.Language.Term.liftAt

{L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → (n' : ℕ) → ℕ → L.Term (α ⊕ Fin n) → L.Term (α ⊕ Fin (n + n'))

Raises all of the Fin-indexed variables of a term greater than or equal to m by n'.

Defined in

Mathlib.ModelTheory.Syntax

Cited by

3 results in Mathlib

Foundations

Depth 19 from the axioms · uses no axioms