filter_add_not — Mathlib

English

The sum of a p-filter and the p-complement filter equals the original multiset.

Русский

Сумма фильтра по p и фильтра по ¬p даёт исходное мультимножество.

LaTeX

$$$\\mathrm{filter}_p(s) + \\mathrm{filter}_{\\lnot p}(s) = s$$$

Lean4

theorem filter_add_not (s : Multiset α) : filter p s + filter (fun a => ¬p a) s = s :=
  by
  rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2]
  · simp only [Multiset.add_zero]
  · simp [-Bool.not_eq_true, -not_and]
  · simp only [implies_true, Decidable.em]

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