suffix_union_right

Mathlib.Data.List.Lattice

URI: https://scilib.ai/kg/mathlib#List.suffix_union_right

English

l2 is a suffix of l1 ∪ l2.

Русский

l2 является суффиксом l1 ∪ l2.

LaTeX

$$$$ l_2 \\text{ is a suffix of } l_1 \\cup l_2. $$$$

Lean4

theorem suffix_union_right (l₁ l₂ : List α) : l₂ <:+ l₁ ∪ l₂ :=
  (sublist_suffix_of_union l₁ l₂).imp fun _ => And.right

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru