filter

Mathlib.Data.List.Nodup

URI: https://scilib.ai/kg/mathlib#List.Nodup.filter

English

Filtering a nodup list by a Bool predicate preserves nodup.

Русский

Фильтрация списка без повторов по булеву предикату сохраняет безповторность.

LaTeX

$$$\\operatorname{Nodup}(l) \\rightarrow \\operatorname{Nodup}(\\operatorname{filter}(p,l))$$$

Lean4

theorem filter (p : α → Bool) {l} : Nodup l → Nodup (filter p l) := by simpa using Pairwise.filter p

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

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

Разделы

Аффилиация

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