trans_left — Mathlib

English

If a TransGen from a to b and a RefTransGen from b to c, then a TransGen from a to c.

Русский

Если имеется TransGen r a b и ReflTransGen r b c, то есть TransGen r a c.

LaTeX

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

Lean4

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

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