filter_cons_of_neg

Mathlib.Data.Multiset.Filter

URI: https://scilib.ai/kg/mathlib#Multiset.filter_cons_of_neg

← MathLib Explorer

English

If not p(a), then filter p (a :: s) = filter p s.

Русский

Если не p(a), то filter p (a :: s) = filter p s.

LaTeX

$$$\\neg p(a) \\Rightarrow \\mathrm{filter}_p(\\{a\\} \\u2220 s) = \\mathrm{filter}_p(s)$$$

Lean4

@[simp]
theorem filter_cons_of_neg {a : α} (s) : ¬p a → filter p (a ::ₘ s) = filter p s :=
  Quot.inductionOn s fun _ h => congr_arg ofList <| List.filter_cons_of_neg <| by simpa using h

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

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

Разделы

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

Аффилиация

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