cons_cons — Mathlib

English

Let l1 and l2 be lists and a an element. If l1 is a sublist of l2, then the lists a :: l1 and a :: l2 satisfy a :: l1 <+ a :: l2.

Русский

Пусть l1 и l2 — списки, а а — элемент. Если l1 является подпоследовательностью (подсписком) l2, то a :: l1 является подпоследовательностью a :: l2.

LaTeX

$$$ \forall a : \alpha,\; \forall l_1,l_2 : \text{List }\alpha,\; l_1 <+ l_2 \implies (a :: l_1) <+ (a :: l_2) $$$

Lean4

theorem cons_cons {l₁ l₂ : List α} (a : α) (s : l₁ <+ l₂) : a :: l₁ <+ a :: l₂ :=
  Sublist.cons₂ _ s

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