tail_sublistForall₂_self — Mathlib

English

For any list l and reflexive relation Rₐ, the tail of l is related to l by SublistForall₂ Rₐ.

Русский

Для любого списка l и рефлексивного отношения Rₐ хвост списка l связан с самим списком через SublistForall₂.

LaTeX

$$$$\\text{TailSublistForall2}: \\forall l:\\, \\text{List }\\ α,\\ SublistForall₂\\ R_α\\ (l.tail)\\ (l). $$$$

Lean4

theorem tail_sublistForall₂_self [IsRefl α Rₐ] (l : List α) : SublistForall₂ Rₐ l.tail l :=
  l.tail_sublist.sublistForall₂

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