dropSlice_subset — Mathlib

English

For any n,m,l, the set of elements of l.dropSlice n m is contained in the set of elements of l.

Русский

Для любых n,m,l множество элементов l.dropSlice n m содержится во множестве элементов l.

LaTeX

$$$\forall n,m : \mathbb{N}, \forall l : \text{List}(\alpha),\; l.dropSlice(n,m) \subseteq l.$$$

Lean4

theorem dropSlice_subset (n m : ℕ) (l : List α) : l.dropSlice n m ⊆ l :=
  (dropSlice_sublist n m l).subset

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