filter_neg — Mathlib

English

Filtering the negation interacts with the positive filter by linearity: filter p of -f equals the negation of filter p f.

Русский

Фильтрация по p и отрицанию взаимодействуют линейно: фильтр p(-f) = -(фильтр p f).

LaTeX

$$$$ \\text{filter } p (-f) = -\\text{filter } p f. $$$$

Lean4

@[simp]
theorem filter_neg (p : α → Prop) [DecidablePred p] (f : α →₀ G) : filter p (-f) = -filter p f :=
  (filterAddHom p : (_ →₀ G) →+ _).map_neg f

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