Theorems · Theorem · logic and foundations

FirstOrder.Language.Term.realize_restrictVarLeft

∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} [inst_1 : DecidableEq α]
  {γ : Type u_4} {t : L.Term (α ⊕ γ)} {f : ↥t.varFinsetLeft → β} {xs : β ⊕ γ → M} (xs' : α → M),
  (∀ (a : ↥t.varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a) →
    FirstOrder.Language.Term.realize xs (t.restrictVarLeft f) =
      FirstOrder.Language.Term.realize (Sum.elim xs' (xs ∘ Sum.inr)) t

Defined in

Mathlib.ModelTheory.Semantics

Cited by

2 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureDecidableEq