cons_sublist_cons' — Mathlib

English

For lists l1, l2 and elements a, b, the sublist relation between a :: l1 and b :: l2 is equivalent to either a :: l1 is a sublist of l2, or a = b and l1 is a sublist of l2.

Русский

Для списков l1, l2 и элементов a, b отношение подпоследовательности между a :: l1 и b :: l2 эквивалентно либо a :: l1 подпоследовательен l2, либо a = b и l1 подпоследовательен l2.

LaTeX

$$$ (a :: l_1) <+ (b :: l_2) \;\iff\; (a :: l_1) <+ l_2 \\quad\lor\quad (a = b) \wedge (l_1 <+ l_2) $$$

Lean4

theorem cons_sublist_cons' {a b : α} : a :: l₁ <+ b :: l₂ ↔ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂ := by grind

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