instIsTransSetOfProdMatch_1PropOfIsTrans

Mathlib.Data.Rel

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

English

If R is transitive, then the relation {(a,b) | R a b} is transitive.

Русский

Если R транзитивно, то отношение {(a,b) | R a b} транзитивно.

LaTeX

$$If IsTrans α R, then SetRel.IsTrans {(a,b) | R a b}$$

Lean4

instance {R : α → α → Prop} [IsTrans α R] : SetRel.IsTrans {(a, b) | R a b} :=
  ‹_›

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

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

Разделы

Аффилиация

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