filter_cons — Mathlib

English

Filters commute: applying filter by p and q in either order gives the same result.

Русский

Фильтры взаимно приводят к одинаковому результату: фильтрацию по p и по q можно применять в любом порядке.

LaTeX

$$$\\mathrm{filter}_p(\\mathrm{filter}_q(s)) = \\mathrm{filter}_q(\\mathrm{filter}_p(s))$$

Lean4

theorem filter_cons {a : α} (s : Multiset α) : filter p (a ::ₘ s) = (if p a then { a } else 0) + filter p s :=
  by
  split_ifs with h
  · rw [filter_cons_of_pos _ h, singleton_add]
  · rw [filter_cons_of_neg _ h, Multiset.zero_add]

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