subset_dedup

Mathlib.Data.List.Dedup

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

English

Every element of l is present in dedup(l); i.e., l is a subset of dedup(l) in the sense of element membership.

Русский

Каждый элемент списка l встречается в dedup(l); то есть l является подмножеством dedup(l) по принадлежности элементов.

LaTeX

$$$l \\subseteq dedup(l)$$$

Lean4

theorem subset_dedup (l : List α) : l ⊆ dedup l := fun _ => mem_dedup.2

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

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

Разделы

Аффилиация

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