mem_of_mem_dropSlice

Mathlib.Data.List.Infix

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

English

If a is an element of l.dropSlice n m, then a is an element of l.

Русский

Если элемент a принадлежит l.dropSlice n m, то он принадлежит l.

LaTeX

$$$\forall n,m : \mathbb{N}, \forall l : \text{List}(\alpha), \forall a : \alpha,\ a \in l.dropSlice(n,m) \Rightarrow a \in l.$$$

Lean4

theorem mem_of_mem_dropSlice {n m : ℕ} {l : List α} {a : α} (h : a ∈ l.dropSlice n m) : a ∈ l :=
  dropSlice_subset n m l h

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

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

Разделы

Аффилиация

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