Theorems · Theorem · logic and foundations

FirstOrder.Language.Formula.realize_rel

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

Defined in

Mathlib.ModelTheory.Semantics

Cited by

2 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.Structure