reflTransGen_eq_reflGen

Mathlib.Logic.Relation

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

English

If r is transitive, the reflexive-transitive closure equals the reflexive generation: ReflTransGen r = ReflGen r.

Русский

Если r транзитивно, то ReflTransGen r = ReflGen r.

LaTeX

$$$\\\\operatorname{ReflTransGen}(r) = \\\\operatorname{ReflGen}(r)$$$

Lean4

theorem reflTransGen_eq_reflGen (hr : Transitive r) : ReflTransGen r = ReflGen r := by
  rw [← reflGen_transGen, transGen_eq_self hr]

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

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

Разделы

Аффилиация

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