reflexive — Mathlib

English

Let r be a binary relation symbol. The statement asserts that r is reflexive, i.e., for every x, r(x, x) holds.

Русский

Пусть r — бинарный символ отношения. Утверждение говорит о рефлексивности: для любого x выполнено r(x, x).

LaTeX

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

Lean4

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

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