trans_right — Mathlib

English

If a reflexive-transitive relation holds from a to b and TransGen r b c holds, then TransGen r a c holds.

Русский

Если ReflTransGen r a b и TransGen r b c, то TransGen r a c.

LaTeX

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

Lean4

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

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