English
Let R be a binary relation symbol and t1, t2 be terms in the language. For any structure M and any assignments v : α → M and xs : Fin l → M, the interpretation of the bounded formula R(t1, t2) under v, xs equals the evaluation of R at the evaluations t1(v, xs) and t2(v, xs).
Русский
Пусть R — двоичный символь отношения, а t1, t2 — термы. Для любой структуры M и любых отображений v: α → M и xs: Fin l → M смысл формулы R(t1, t2) определяется как значение отношения R на значениях t1(v, xs) и t2(v, xs).
LaTeX
$$$ (R\text{(boundedFormula)}_{2} \; t_1\; t_2)^{\mathcal{M}}(v, xs) \iff R^{\mathcal{M}}\big( t_1^{\mathcal{M}}(v, xs),\; t_2^{\mathcal{M}}(v, xs) \big) $$$
Lean4
@[simp]
theorem realize_rel₂ {R : L.Relations 2} {t₁ t₂ : L.Term _} :
(R.boundedFormula₂ t₁ t₂).Realize v xs ↔ RelMap R ![t₁.realize (Sum.elim v xs), t₂.realize (Sum.elim v xs)] :=
by
rw [Relations.boundedFormula₂, 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]
