append_subset_of_subset_of_subset

Mathlib.Data.List.Basic

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

← MathLib Explorer

English

If l1 ⊆ l and l2 ⊆ l, then l1 ++ l2 ⊆ l.

Русский

Если l1 ⊆ l и l2 ⊆ l, то l1 ++ l2 ⊆ l.

LaTeX

$$$$\\forall l_1\\, l_2\\, l,\\ l_1 \\subseteq l \\land l_2 \\subseteq l \\rightarrow l_1 ++ l_2 \\subseteq l.$$$$

Lean4

theorem append_subset_of_subset_of_subset {l₁ l₂ l : List α} (l₁subl : l₁ ⊆ l) (l₂subl : l₂ ⊆ l) : l₁ ++ l₂ ⊆ l :=
  fun _ h ↦ (mem_append.1 h).elim (@l₁subl _) (@l₂subl _)

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

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

Разделы

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

Аффилиация

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