filter_sub — Mathlib

English

Filtering commutes with subtraction: filter p (f1 − f2) = filter p f1 − filter p f2.

Русский

Фильтрация коммутирует с вычитанием: фильтр p (f1 − f2) = фильтр p f1 − фильтр p f2.

LaTeX

$$$$ \\mathrm{filter}\ p (f_1 - f_2) = \\mathrm{filter}\ p f_1 - \\mathrm{filter}\ p f_2. $$$$

Lean4

@[simp]
theorem filter_sub (p : α → Prop) [DecidablePred p] (f₁ f₂ : α →₀ G) : filter p (f₁ - f₂) = filter p f₁ - filter p f₂ :=
  (filterAddHom p : (_ →₀ G) →+ _).map_sub f₁ f₂

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