filter_ne_eq_erase'

Mathlib.Data.DFinsupp.Defs

URI: https://scilib.ai/kg/mathlib#DFinsupp.filter_ne_eq_erase'

← MathLib Explorer

English

Same as above: f.filter (i ≠ ·) = f.erase i.

Русский

То же самое: f.filter (i ≠ ·) = f.erase i.

LaTeX

$$$ f.filter (i \\\\neq \\\\cdot) = f.\\\\mathrm{erase} i $$$

Lean4

@[simp]
theorem filter_ne_eq_erase' (f : Π₀ i, β i) (i : ι) : f.filter (i ≠ ·) = f.erase i :=
  by
  rw [← filter_ne_eq_erase f i]
  congr with j
  exact ne_comm

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

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

Разделы

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

Аффилиация

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