Theorems · Theorem · logic and foundations

FirstOrder.Language.Term.restrictVarLeft.eq_def

∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] {γ : Type u_2} (x : L.Term (α ⊕ γ))
  (x_1 : ↥x.varFinsetLeft → β),
  x.restrictVarLeft x_1 =
    match x, x_1 with
    | FirstOrder.Language.var (Sum.inl a), f => FirstOrder.Language.var (Sum.inl (f ⟨a, ⋯⟩))
    | FirstOrder.Language.var (Sum.inr a), _f => FirstOrder.Language.var (Sum.inr a)
    | FirstOrder.Language.func F ts, f =>
      FirstOrder.Language.func F fun i => (ts i).restrictVarLeft (f ∘ Set.inclusion ⋯)

Defined in

Mathlib.ModelTheory.Semantics

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEq