filter

Mathlib.Data.Multiset.Filter

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

English

If a multiset is nodup, then filtering it by any predicate preserves nodupness.

Русский

Если мультисет не имеет повторов, фильтрация его сохраняет это свойство.

LaTeX

$$$ \\text{Nodup}(s) \\rightarrow \\text{Nodup}(\\mathrm{filter}\\ p\\ s) $$$

Lean4

theorem filter (p : α → Prop) [DecidablePred p] {s} : Nodup s → Nodup (filter p s) :=
  Quot.induction_on s fun _ => List.Nodup.filter (p ·)

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

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

Разделы

Аффилиация

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