filterAddMonoidHom

Mathlib.Data.DFinsupp.Defs

URI: https://scilib.ai/kg/mathlib#DFinsupp.filterAddMonoidHom

Lean4

/-- `DFinsupp.filter` as an `AddMonoidHom`. -/
@[simps]
def filterAddMonoidHom [∀ i, AddZeroClass (β i)] (p : ι → Prop) [DecidablePred p] : (Π₀ i, β i) →+ Π₀ i, β i
    where
  toFun := filter p
  map_zero' := filter_zero p
  map_add' := filter_add p

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

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

Разделы

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

Аффилиация

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