transitive_transGen

Mathlib.Logic.Relation

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

English

TransGen r is transitive; if a → b and b → c via TransGen, then a → c via TransGen.

Русский

TransGen r транзитивно: если a ~> b и b ~> c через TransGen, то a ~> c через TransGen.

LaTeX

$$$ \forall {α} {r : α \to α \to \mathrm{Prop}} {a b c : α}, \mathrm{TransGen} r a b \to \mathrm{TransGen} r b c \to \mathrm{TransGen} r a c $$$

Lean4

theorem transitive_transGen : Transitive (TransGen r) := fun _ _ _ ↦ TransGen.trans

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

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

Разделы

Аффилиация

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