transitive_of_trans — Mathlib

English

Let r be a binary relation on α. If r is transitive, then for all a,b,c ∈ α, r(a,b) and r(b,c) imply r(a,c).

Русский

Пусть r — бинарное отношение на α. Если r транзитивно, то для любых a,b,c ∈ α верно: r(a,b) и r(b,c) ⇒ r(a,c).

LaTeX

$$$\\\\forall a,b,c \\\\in \\\\alpha, \\\\ r a b \\\\to \\\\ r b c \\\\to \\\\ r a c$$$

Lean4

theorem transitive_of_trans (r : α → α → Prop) [IsTrans α r] : Transitive r :=
  IsTrans.trans

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