union_sublist_append

Mathlib.Data.List.Lattice

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

← MathLib Explorer

English

The union l1 ∪ l2 is a sublist of l1 ++ l2.

Русский

Объединение l1 ∪ l2 является подпоследовательностью l1 ++ l2.

LaTeX

$$$$ l_1 \\cup l_2 <+ l_1 ++ l_2. $$$$

Lean4

theorem union_sublist_append (l₁ l₂ : List α) : l₁ ∪ l₂ <+ l₁ ++ l₂ :=
  let ⟨_, s, e⟩ := sublist_suffix_of_union l₁ l₂
  e ▸ (append_sublist_append_right _).2 s

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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