filter_cons_of_neg

Mathlib.Data.Finset.Basic

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

← MathLib Explorer

English

If a ∉ s and p(a) is false, then filter p (cons a s ha) = filter p s.

Русский

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

LaTeX

$$$\\neg p(a) \\Rightarrow \\operatorname{filter}(p, \\{a\\} \\cup S) = \\operatorname{filter}(p, S)$$$

Lean4

theorem filter_cons_of_neg (a : α) (s : Finset α) (ha : a ∉ s) (hp : ¬p a) : filter p (cons a s ha) = filter p s :=
  eq_of_veq <| Multiset.filter_cons_of_neg s.val hp

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

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

Разделы

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

Аффилиация

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