tail' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem tail' (hab : ReflTransGen r a b) (hbc : r b c) : TransGen r a c := by
  induction hab generalizing c with
  | refl => exact single hbc
  | tail _ hdb IH => exact tail (IH hdb) hbc

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