trans

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.trans

English

If a is related to b and b to c by a transitive relation, then a is related to c.

Русский

Если a связано с b, а b связано с c по транзитивному отношению, то a связано с c.

LaTeX

$$$a \\sim_R b \\to b \\sim_R c \\to a \\sim_R c$$$

Lean4

protected theorem trans [R.IsTrans] (hab : a ~[R] b) (hbc : b ~[R] c) : a ~[R] c :=
  trans_of (· ~[R] ·) hab hbc

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru