Theorems · Definition · logic and foundations

FirstOrder.Language.Term.restrictVarLeft

{L : FirstOrder.Language} →
  {α : Type u'} →
    {β : Type v'} →
      [inst : DecidableEq α] → {γ : Type u_2} → (t : L.Term (α ⊕ γ)) → (↥t.varFinsetLeft → β) → L.Term (β ⊕ γ)

Restricts a term to use only a set of the given variables on the left side of a sum.

Defined in

Mathlib.ModelTheory.Syntax

Cited by

5 results in Mathlib

Foundations

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

Assumes

DecidableEq