English
Let R be a unary relation symbol in a first-order language L and t a term. For any L-structure M and any interpretation v of the variables, the truth value of R(t) under v is exactly the membership of t(v) in the interpretation of R in M.
Русский
Пусть R — унарное отношение языка L и t — терм. Для любой структуры M и любых подстановок v: α → M истиненность R(t) векторной подстановки равна принадлежности t(v) достаточно к интерпретации R в M.
LaTeX
$$$ (R(t))^M(v) \iff t^M(v) \in R^M $$$
Lean4
@[simp]
theorem realize_rel₁ {R : L.Relations 1} {t : L.Term _} : (R.formula₁ t).Realize v ↔ RelMap R ![t.realize v] :=
by
rw [Relations.formula₁, realize_rel, iff_eq_eq]
refine congr rfl (funext fun _ => ?_)
simp only [Matrix.cons_val_fin_one]
