single

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Relation.ReflTransGen.single

English

If a is related to b by r, then a is related to b by the reflexive-transitive closure of r.

Русский

Если a связан с b отношением r, то a связан с b тем же замыканием рефлексивно-переходного замыкания.

LaTeX

$$$ ∀ \{α\} {r : α \to α \to \mathrm{Prop}} {a b : α}, r a b \to \mathrm{ReflTransGen} r a b $$$

Lean4

theorem single (hab : r a b) : ReflTransGen r a b :=
  refl.tail hab

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

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

Разделы

Аффилиация

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