head — Mathlib

English

If a is related to b by r and b is related to c by ReflTransGen, then a is related to c by ReflTransGen.

Русский

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

LaTeX

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

Lean4

theorem head (hab : r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by
  induction hbc with
  | refl => exact refl.tail hab
  | tail _ hcd hac => exact hac.tail hcd

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