English
Filtering by p after filtering by q yields the same result as filtering by q after filtering by p, i.e., the order of applying two boolean filters on a list does not matter.
Русский
Фильтрация по p после фильтрации по q даёт тот же результат, что и фильтрация по q после фильтрации по p; порядок применения двух булевых фильтров к списку не влияет на результат.
LaTeX
$$$ \\forall p,q:\\alpha\\to\\Bool,\\; \\text{filter}\\,p\\ (\\text{filter}\\,q\\ l) = \\text{filter}\\,q\\ (\\text{filter}\\,p\\ l) $$$
Lean4
theorem filter_comm (q) (l : List α) : filter p (filter q l) = filter q (filter p l) := by simp [Bool.and_comm]
