Destuttering of Lists #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file proves theorems about
data.list.defs), which greedily removes all
non-related items that are adjacent in a list, e.g.
[2, 2, 3, 3, 2].destutter (≠) = [2, 3, 2].
Note that we make no guarantees of being the longest sublist with this property; e.g.,
[123, 1, 2, 5, 543, 1000].destutter (<) = [123, 543, 1000], but a longer ascending chain could be
[1, 2, 5, 543, 1000].
Main statements #
l.destutteris a sublist of
- Analogies of these theorems for
list.destutter', which is the
adjacent, chain, duplicates, remove, list, stutter, destutter