symmetric — Mathlib

English

Let r be a binary relation symbol. The sentence states that r is symmetric: for all x,y, r(x,y) implies r(y,x).

Русский

Пусть r — бинарная связь. Утверждение: симметричность: для любых x,y верно r(x,y) ⇒ r(y,x).

LaTeX

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

Lean4

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

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