English
Let R be a binary relation symbol and t1, t2 terms. For any M and v, the truth of R(t1, t2) under v is exactly the membership of (t1(v), t2(v)) in the interpretation of R in M.
Русский
Пусть R — бинарное отношение и t1, t2 — термы. Для любой структуры M и подстановки v истина R(t1, t2) равна принадлежности пары (t1(v), t2(v)) интерпретации R в M.
LaTeX
$$$ (R(t_1,t_2))^M(v) \iff (t_1^M(v), t_2^M(v)) \in R^M $$$
Lean4
@[simp]
theorem realize_rel₂ {R : L.Relations 2} {t₁ t₂ : L.Term _} :
(R.formula₂ t₁ t₂).Realize v ↔ RelMap R ![t₁.realize v, t₂.realize v] :=
by
rw [Relations.formula₂, realize_rel, iff_eq_eq]
refine congr rfl (funext (Fin.cases ?_ ?_))
· simp only [Matrix.cons_val_zero]
· simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]
