to_reflTransGen

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Relation.TransGen.to_reflTransGen

← MathLib Explorer

English

Every TransGen proof yields a ReflTransGen proof.

Русский

Любое доказательство TransGen даёт доказательство ReflTransGen.

LaTeX

$$$ \forall {α} {r} {a b}, TransGen r a b \to ReflTransGen r a b $$$

Lean4

theorem to_reflTransGen {a b} (h : TransGen r a b) : ReflTransGen r a b := by
  induction h with
  | single h => exact ReflTransGen.single h
  | tail _ bc ab => exact ReflTransGen.tail ab bc

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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