instIsTransReflTransGen

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Relation.instIsTransReflTransGen

English

The relation ReflTransGen r is transitive.

Русский

Отношение ReflTransGen r транзитивно.

LaTeX

$$$$\\text{IsTrans }\\alpha (\\operatorname{ReflTransGen} r)$$$$

Lean4

instance : IsTrans α (ReflTransGen r) :=
  ⟨@ReflTransGen.trans α r⟩

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

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

Разделы

Аффилиация

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