cons_subset_of_subset_of_mem

Mathlib.Data.List.Basic

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

English

If a ∈ m and l ⊆ m, then a :: l ⊆ m.

Русский

Если a ∈ m и l ⊆ m, то a :: l ⊆ m.

LaTeX

$$$$\\forall a\\, l\\, m,\\ a \\in m \\\\rightarrow l \\subseteq m \\\\rightarrow a :: l \\subseteq m.$$$$

Lean4

theorem cons_subset_of_subset_of_mem {a : α} {l m : List α} (ainm : a ∈ m) (lsubm : l ⊆ m) : a :: l ⊆ m :=
  cons_subset.2 ⟨ainm, lsubm⟩

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

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

Разделы

Аффилиация

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