filter_filter — Mathlib

English

Filtering twice is equivalent to filtering by the conjunction: p a ∧ q a.

Русский

Повторная фильтрация эквивалентна фильтрации по конъюнкции предикатов p и q.

LaTeX

$$$\\mathrm{filter}_p(\\mathrm{filter}_q(s)) = \\mathrm{filter}_{\\lambda a. (p(a) \\land q(a))}(s)$$$

Lean4

@[simp]
theorem filter_filter (q) [DecidablePred q] (s : Multiset α) : filter p (filter q s) = filter (fun a => p a ∧ q a) s :=
  Quot.inductionOn s fun l => by simp

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