Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.realize_rel

∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M}
  {k : ℕ} {R : L.Relations k} {ts : Fin k → L.Term (α ⊕ Fin l)},
  (R.boundedFormula ts).Realize v xs ↔
    FirstOrder.Language.Structure.RelMap R fun i => FirstOrder.Language.Term.realize (Sum.elim v xs) (ts i)

Defined in

Mathlib.ModelTheory.Semantics

Cited by

3 results in Mathlib

Foundations

Depth 21 from the axioms · uses no axioms

Assumes

FirstOrder.Language.Structure