English
Let r be a relation on a set α. If a is related to b by the reflexive-transitive closure of r, and b is related to c by the same closure, then a is related to c by the reflexive-transitive closure.
Русский
Пусть r — бинарное отношение на множестве α. Если a связан с b отношением рефлексивно-переходного замыкания r, а b связан с c тем же замыканием, то a связан с c этим замыканием.
LaTeX
$$$ ∀ \{α\} {r : α \to α \to \mathrm{Prop}} {a b c : α}, \mathrm{ReflTransGen} r a b \to \mathrm{ReflTransGen} r b c \to \mathrm{ReflTransGen} r a c $$$
Lean4
@[trans]
theorem trans (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by
induction hbc with
| refl => assumption
| tail _ hcd hac => exact hac.tail hcd
