filterAddHom

Mathlib.Data.Finsupp.Basic

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

Lean4

/-- `Finsupp.filter` as an `AddMonoidHom`. -/
def filterAddHom (p : α → Prop) [DecidablePred p] : (α →₀ M) →+ α →₀ M
    where
  toFun := filter p
  map_zero' := filter_zero p
  map_add' f
    g :=
    DFunLike.coe_injective <| by
      simp_rw [coe_add, filter_eq_indicator]
      exact Set.indicator_add {x | p x} f g

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

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

Разделы

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

Аффилиация

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