Theorems · Definition · logic and foundations

FirstOrder.Language.Term.constantsVarsEquivLeft

{L : FirstOrder.Language} →
  {α : Type u'} → {β : Type v'} → {γ : Type u_1} → (L.withConstants γ).Term (α ⊕ β) ≃ L.Term ((γ ⊕ α) ⊕ β)

A bijection between terms with constants and terms with extra variables.

Defined in

Mathlib.ModelTheory.Syntax

Cited by

3 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound