irreflexive — Mathlib

English

Let r be a binary relation symbol. The sentence states that r is irreflexive, i.e., for every x, not r(x, x).

Русский

Пусть r — бинарное отношение. Утверждение: irreflexive, то есть для всех x не выполняется r(x, x).

LaTeX

$$$\\\\forall x\\\\, \\\\neg r(x,x)$$$

Lean4

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

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