dedup_cons_of_mem'

Mathlib.Data.List.Dedup

URI: https://scilib.ai/kg/mathlib#List.dedup_cons_of_mem'

← MathLib Explorer

English

If a belongs to dedup l, then dedup (a :: l) equals dedup l.

Русский

Если a входит в dedup l, то dedup (a :: l) = dedup l.

LaTeX

$$$$ (a \\in dedup\\ l) \\Rightarrow dedup (a :: l) = dedup\\ l. $$$$

Lean4

theorem dedup_cons_of_mem' {a : α} {l : List α} (h : a ∈ dedup l) : dedup (a :: l) = dedup l :=
  pwFilter_cons_of_neg <| by simpa only [forall_mem_ne, not_not] using h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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