filter_sub — Mathlib

English

Let p be a decidable predicate on ι and f,g be finitely supported functions with values in β i. Then filtering distributes over subtraction: (f - g).filter p = f.filter p - g.filter p.

Русский

Пусть p — разрешимый предикат на ι, а f,g — конечно-поддерживаемые функции. Тогда фильтрация распределяется по вычитанию: (f − g).filter p = f.filter p − g.filter p.

LaTeX

$$$ (f - g).filter p = f.filter p - g.filter p $$$

Lean4

@[simp]
theorem filter_sub [∀ i, AddGroup (β i)] (p : ι → Prop) [DecidablePred p] (f g : Π₀ i, β i) :
    (f - g).filter p = f.filter p - g.filter p :=
  (filterAddMonoidHom β p).map_sub f g

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