English
Let M be an L-structure for a language with a binary relation symbol r. The sentence r.total expresses that the interpretation of r is total on M, i.e., for all a,b in M, either r(a,b) or r(b,a). The model M satisfies this sentence exactly when the interpretation of r on M is a total relation.
Русский
Пусть M — структура языка L с бинарным отношением r. Предикат r.total утверждает, что для всяких x,y ∈ M выполняется либо r(x,y), либо r(y,x). Тогда M удовлетворяет r.total тогда и только тогда, когда интерпретация r в M образует полное (тотальное) отношение на M.
LaTeX
$$$M \vDash r.{\rm total} \iff \forall x,y \in M,\; R_r(x,y) \lor R_r(y,x),$$$
Lean4
@[simp]
theorem realize_total : M ⊨ r.total ↔ Total fun x y : M => RelMap r ![x, y] :=
forall_congr' fun _ => forall_congr' fun _ => realize_sup.trans (or_congr realize_rel₂ realize_rel₂)
