filter_comm — Mathlib

English

The sum of p-filter and q-filter equals the sum of the p∨q-filter and the p∧q-filter.

Русский

Сумма фильтров по p и по q равна сумме фильтров по p∨q и p∧q.

LaTeX

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

Lean4

theorem filter_comm (q) [DecidablePred q] (s : Multiset α) : filter p (filter q s) = filter q (filter p s) := by
  simp [and_comm]

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