filter_single_of_neg

Mathlib.Data.Finsupp.Basic

URI: https://scilib.ai/kg/mathlib#Finsupp.filter_single_of_neg

← MathLib Explorer

English

If not p(a), filtering a singleton at a yields zero.

Русский

Если не p(a), фильтрация синглтона (a, b) по p даёт нуль.

LaTeX

$$$$ \\neg p(a) \\to (\\mathrm{single}\ a\ b).\\mathrm{filter}\\ p = 0. $$$$

Lean4

@[simp]
theorem filter_single_of_neg {a : α} {b : M} (h : ¬p a) : (single a b).filter p = 0 :=
  (filter_eq_zero_iff _ _).2 fun _ hpx => single_apply_eq_zero.2 fun hxa => absurd hpx (hxa.symm ▸ h)

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

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

Разделы

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

Аффилиация

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