dedup_sublist — Mathlib

English

For any list l, the deduplicated version dedup(l) is a sublist of l (i.e., can be obtained by deleting some elements from l while preserving the remaining order).

Русский

Для любого списка l упрощённая версия dedup(l) является подпоследовательностью списка l (можно получить удалением элементов из l без нарушения порядка оставшихся).

LaTeX

$$$\\mathrm{dedup}(l) \\sqsubseteq l$$$

Lean4

theorem dedup_sublist : ∀ l : List α, dedup l <+ l :=
  pwFilter_sublist

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