dedup_subset — Mathlib

English

For every list l, the deduplicated list contains only elements that appear in l; i.e., dedup(l) is contained in l as a multiset of elements.

Русский

Для каждого списка l упорядоченный список после удаления повторов содержит только элементы, встречающиеся в l; то есть dedup(l) содержится в l как множество элементов.

LaTeX

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

Lean4

theorem dedup_subset : ∀ l : List α, dedup l ⊆ l :=
  pwFilter_subset

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