transitive — Mathlib

English

Let r be a binary relation symbol. The sentence states that r is transitive: if r(x,y) and r(y,z), then r(x,z).

Русский

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

LaTeX

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

Lean4

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

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