antisymmetric — Mathlib

English

Let r be a binary relation symbol. The sentence says that r is antisymmetric: if r(x,y) and r(y,x), then x = y.

Русский

Пусть r — бинарное отношение. Антисимметричность: если r(x,y) и r(y,x), то x = y.

LaTeX

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

Lean4

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

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