total — Mathlib

English

Let r be a binary relation symbol. The sentence asserts totality of r: for all x,y, either r(x,y) or r(y,x).

Русский

Пусть r — бинарное отношение. Тотальность: для всех x,y либо r(x,y), либо r(y,x).

LaTeX

$$$\\\\forall x\\\\forall y\\\\ (r(x,y) \\\\lor r(y,x))$$$

Lean4

/-- The sentence indicating that a basic relation symbol is total. -/
protected def total : L.Sentence :=
  ∀'∀'(r.boundedFormula₂ (&0) &1 ⊔ r.boundedFormula₂ (&1) &0)

Похожие утверждения